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  437  pm5.19  654  con4biddc  787  con1biimdc  800  bijadc  809  pclem6  1305  albi  1397  exbi  1535  equsexd  1657  cbv2h  1674  sbiedh  1710  eumo0  1972  ceqsalt  2625  vtoclgft  2649  spcgft  2675  pm13.183  2732  reu6  2781  reu3  2782  sbciegft  2844  ddifstab  3104  fv3  5218  prnmaxl  6678  prnminu  6679  elabgft1  10588  elabgf2  10590  bj-axemptylem  10683  bj-notbi  10716  bj-inf2vn  10769  bj-inf2vn2  10770  bj-nn0sucALT  10773