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	|- ( ( ph <-> ps ) -> ( ph -> ps ) )

Proof of Theorem bi1

Step	Hyp	Ref	Expression
1		df-bi 115	. . 3 |- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2	1	simpli 109	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3	2	simpld 110	1 |- ( ( ph <-> ps ) -> ( ph -> ps ) )

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  657  con4biddc  792  con1biimdc  805  bijadc  814  pclem6  1310  albi  1402  exbi  1540  equsexd  1664  cbv2h  1681  sbiedh  1717  eumo0  1979  ceqsalt  2645  vtoclgft  2669  spcgft  2696  pm13.183  2754  reu6  2804  reu3  2805  sbciegft  2869  ddifstab  3132  fv3  5328  prnmaxl  7047  prnminu  7048  elabgft1  11678  elabgf2  11680  bj-axemptylem  11783  bj-notbi  11816  bj-inf2vn  11869  bj-inf2vn2  11870  bj-nn0sucALT  11873