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  1492  exbi  1628  equsexd  1753  cbv2h  1772  cbv2w  1774  sbiedh  1811  eumo0  2086  ceqsalt  2803  vtoclgft  2828  spcgft  2857  pm13.183  2918  reu6  2969  reu3  2970  sbciegft  3036  ddifstab  3313  exmidsssnc  4263  fv3  5622  prnmaxl  7636  prnminu  7637  elabgft1  15914  elabgf2  15916  bj-axemptylem  16027  bj-inf2vn  16109  bj-inf2vn2  16110  bj-nn0sucALT  16113