IFF

The constant "iff" expresses logical equivalence.

Systems

LRC_F

Typed Forward Strict

↔E: Biconditional Elimination↔I: Biconditional Introduction

Point And Click

↔E: Biconditional Elimination↔I: Biconditional Introduction

OLI

Point And Click

↔I: Biconditional Introduction↔EL: Biconditional Elimination Left↔ER: Biconditional Elimination Right

The Logic Book

Point And Click

≡E: Biconditional Elimination≡I: Biconditional IntroductionEquiv: Equivalence

LRC

Typed Forward Strict

≡E: Biconditional Elimination≡I: Biconditional Introduction

Point And Click

≡E: Biconditional Elimination≡I: Biconditional Introduction

LRC_P

Typed Forward Strict

↔E: Biconditional Elimination↔I: Biconditional Introduction

Point And Click

↔E: Biconditional Elimination↔I: Biconditional Introduction

LRC_O

Typed Forward Strict

↔E: Biconditional Elimination↔I: Biconditional Introduction

Point And Click

↔E: Biconditional Elimination↔I: Biconditional Introduction