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  667  pm5.19  707  con4biddc  858  con1biimdc  874  bijadc  883  pclem6  1385  albi  1479  exbi  1615  equsexd  1740  cbv2h  1759  cbv2w  1761  sbiedh  1798  eumo0  2069  ceqsalt  2778  vtoclgft  2802  spcgft  2829  pm13.183  2890  reu6  2941  reu3  2942  sbciegft  3008  ddifstab  3282  exmidsssnc  4218  fv3  5554  prnmaxl  7512  prnminu  7513  elabgft1  14968  elabgf2  14970  bj-axemptylem  15082  bj-inf2vn  15164  bj-inf2vn2  15165  bj-nn0sucALT  15168