MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bi1 Unicode version

Theorem bi1 186
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
Assertion
Ref Expression
bi1

Proof of Theorem bi1
StepHypRef Expression
1 df-bi 185 . . 3
2 simplim 151 . . 3
31, 2ax-mp 5 . 2
4 simplim 151 . 2
53, 4syl 16 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184
This theorem is referenced by:  biimpi  194  bicom1  199  biimpd  207  ibd  243  pm5.74  244  bi3antOLD  289  pm5.501  341  bija  355  bianir  967  albi  1639  exbi  1666  cbv2h  2019  equveliOLD  2089  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  eumo0OLD  2317  2eu6  2383  2eu6OLD  2384  eleq2d  2527  ceqsalt  3132  vtoclgft  3157  spcgft  3186  pm13.183  3240  reu6  3288  reu3  3289  sbciegft  3358  fv3  5884  expeq0  12196  t1t0  19849  kqfvima  20231  ufileu  20420  cvmlift2lem1  28747  btwndiff  29677  nn0prpw  30141  bi33imp12  33259  bi23imp1  33264  bi123imp0  33265  eqsbc3rVD  33640  imbi12VD  33673  2uasbanhVD  33711  bj-dfbi6  34156  bj-bi3ant  34178  bj-cbv2hv  34294  bj-eumo0  34414  bj-ceqsalt0  34449  bj-ceqsalt1  34450  bj-ax9  34464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator