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

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

Proof of Theorem bi1
StepHypRef Expression
1 df-bi 115 . . 3 (((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑))) ∧ (((𝜑𝜓) ∧ (𝜓𝜑)) → (𝜑𝜓)))
21simpli 109 . 2 ((𝜑𝜓) → ((𝜑𝜓) ∧ (𝜓𝜑)))
32simpld 110 1 ((𝜑𝜓) → (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  biimpi  118  bicom1  129  biimpd  142  ibd  176  pm5.74  177  bi3ant  222  pm5.501  242  pm5.32d  438  pm5.19  655  con4biddc  788  con1biimdc  801  bijadc  810  pclem6  1306  albi  1398  exbi  1536  equsexd  1658  cbv2h  1675  sbiedh  1711  eumo0  1973  ceqsalt  2626  vtoclgft  2650  spcgft  2676  pm13.183  2733  reu6  2782  reu3  2783  sbciegft  2845  ddifstab  3105  fv3  5229  prnmaxl  6740  prnminu  6741  elabgft1  10766  elabgf2  10768  bj-axemptylem  10868  bj-notbi  10901  bj-inf2vn  10954  bj-inf2vn2  10955  bj-nn0sucALT  10958
 Copyright terms: Public domain W3C validator