ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimp GIF version

Theorem biimp 118
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.)
Assertion
Ref Expression
biimp ((𝜑𝜓) → (𝜑𝜓))

Proof of Theorem biimp
StepHypRef Expression
1 df-bi 117 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 111 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
32simpld 112 1 ((𝜑𝜓) → (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biimpi  120  bicom1  131  biimpd  144  ibd  178  pm5.74  179  bi3ant  224  pm5.501  244  pm5.32d  450  notbi  666  pm5.19  706  con4biddc  857  con1biimdc  873  bijadc  882  pclem6  1374  albi  1468  exbi  1604  equsexd  1729  cbv2h  1748  cbv2w  1750  sbiedh  1787  eumo0  2057  ceqsalt  2763  vtoclgft  2787  spcgft  2814  pm13.183  2875  reu6  2926  reu3  2927  sbciegft  2993  ddifstab  3267  exmidsssnc  4203  fv3  5538  prnmaxl  7486  prnminu  7487  elabgft1  14500  elabgf2  14502  bj-axemptylem  14614  bj-inf2vn  14696  bj-inf2vn2  14697  bj-nn0sucALT  14700
  Copyright terms: Public domain W3C validator