Theorem bi1 186

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)

Assertion

Ref	Expression
bi1

Proof of Theorem bi1

Step	Hyp	Ref	Expression
1		df-bi 185	. . 3
2		simplim 151	. . 3
3	1, 2	ax-mp 5	. 2
4		simplim 151	. 2
5	3, 4	syl 16	1

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