Theorem biimp 118

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

Assertion

Ref	Expression
biimp	|- ( ( ph <-> ps ) -> ( ph -> ps ) )

Proof of Theorem biimp

Step	Hyp	Ref	Expression
1		df-bi 117	. . 3 |- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2	1	simpli 111	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3	2	simpld 112	1 |- ( ( ph <-> ps ) -> ( ph -> ps ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpi  120  bicom1  131  biimpd  144  ibd  178  pm5.74  179  bi3ant  224  pm5.501  244  pm5.32d  450  notbi  668  pm5.19  708  con4biddc  859  con1biimdc  875  bijadc  884  pclem6  1394  albi  1491  exbi  1627  equsexd  1752  cbv2h  1771  cbv2w  1773  sbiedh  1810  eumo0  2085  ceqsalt  2798  vtoclgft  2823  spcgft  2850  pm13.183  2911  reu6  2962  reu3  2963  sbciegft  3029  ddifstab  3305  exmidsssnc  4248  fv3  5601  prnmaxl  7603  prnminu  7604  elabgft1  15751  elabgf2  15753  bj-axemptylem  15865  bj-inf2vn  15947  bj-inf2vn2  15948  bj-nn0sucALT  15951