Theorem bi1 117

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 116	. . 3 |- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2	1	simpli 110	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3	2	simpld 111	1 |- ( ( ph <-> ps ) -> ( ph -> ps ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpi  119  bicom1  130  biimpd  143  ibd  177  pm5.74  178  bi3ant  223  pm5.501  243  pm5.32d  446  notbi  656  pm5.19  696  con4biddc  843  con1biimdc  859  bijadc  868  pclem6  1353  albi  1445  exbi  1584  equsexd  1708  cbv2h  1725  sbiedh  1761  eumo0  2031  ceqsalt  2715  vtoclgft  2739  spcgft  2766  pm13.183  2826  reu6  2877  reu3  2878  sbciegft  2943  ddifstab  3213  exmidsssnc  4134  fv3  5452  prnmaxl  7320  prnminu  7321  elabgft1  13156  elabgf2  13158  bj-axemptylem  13261  bj-inf2vn  13343  bj-inf2vn2  13344  bj-nn0sucALT  13347