Theorem bi2 198

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Assertion

Ref	Expression
bi2

Proof of Theorem bi2

Step	Hyp	Ref	Expression
1		dfbi1 192	. 2
2		simprim 150	. 2
3	1, 2	sylbi 195	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184

This theorem is referenced by:  bicom1  199  pm5.74  244  bi3antOLD  289  bija  355  simplbi2comt  626  pm4.72  876  albi  1639  exbi  1666  cbv2h  2019  equveli  2088  equveliOLD  2089  euex  2308  2eu6  2383  2eu6OLD  2384  eleq2d  2527  ceqsalt  3132  euind  3286  reu6  3288  reuind  3303  sbciegft  3358  axpr  4690  iota4  5574  fv3  5884  nn0prpwlem  30140  nn0prpw  30141  tsbi3  30542  axc11next  31313  pm13.192  31317  exbir  33219  con5  33292  sbcim2g  33309  trsspwALT  33616  trsspwALT2  33617  sspwtr  33619  sspwtrALT  33620  pwtrVD  33624  pwtrrVD  33625  snssiALTVD  33627  sstrALT2VD  33634  sstrALT2  33635  suctrALT2VD  33636  eqsbc3rVD  33640  simplbi2VD  33646  exbirVD  33653  exbiriVD  33654  imbi12VD  33673  sbcim2gVD  33675  simplbi2comtVD  33688  con5VD  33700  2uasbanhVD  33711  bj-bi3ant  34178  bj-cbv2hv  34294  bj-ceqsalt0  34449  bj-ceqsalt1  34450  mapdrvallem2  37372

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