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  666  pm5.19  706  con4biddc  857  con1biimdc  873  bijadc  882  pclem6  1374  albi  1468  exbi  1604  equsexd  1729  cbv2h  1748  cbv2w  1750  sbiedh  1787  eumo0  2057  ceqsalt  2765  vtoclgft  2789  spcgft  2816  pm13.183  2877  reu6  2928  reu3  2929  sbciegft  2995  ddifstab  3269  exmidsssnc  4205  fv3  5540  prnmaxl  7489  prnminu  7490  elabgft1  14615  elabgf2  14617  bj-axemptylem  14729  bj-inf2vn  14811  bj-inf2vn2  14812  bj-nn0sucALT  14815