Theorem biimpd 198

Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
biimpd.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimpd	|- (ph -> (ps -> ch))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 |- (ph -> (ps <-> ch))
2		bi1 178	. 2 |- ((ps <-> ch) -> (ps -> ch))
3	1, 2	syl 15	1 |- (ph -> (ps -> ch))

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  mpbid  201  sylibd  205  sylbid  206  mpbidi  207  syl5ib  210  syl6bi  219  ibi  232  con4bid  284  mtbird  292  mtbiri  294  imbi1d  308  pm5.21im  338  biimpa  470  exintr  1614  spfw  1691  spw  1694  cbvalw  1701  cbvalvw  1702  alcomiw  1704  19.9d  1782  19.23t  1800  dvelimv  1939  dral1  1965  cbval  1984  chvar  1986  spv  1998  sbequi  2059  dral1-o  2154  2eu3  2286  eqrdav  2352  cleqh  2450  ralcom2  2776  ceqsalg  2884  vtoclf  2909  vtocl2  2911  vtocl3  2912  spcdv  2938  rspcdv  2959  elabgt  2983  sbeqalb  3099  ssunsn2  3866  opkthg  4132  iotaval  4351  nnsucelr  4429  tfin11  4494  vfinspss  4552  0cnelphi  4598  iss  5001  tz6.12-1  5345  chfnrn  5400  elpreima  5408  ffnfv  5428  f1elima  5475  ndmovg  5614  enmap2lem3  6066  enmap1lem3  6072  enprmaplem3  6079  enprmaplem5  6081  nnltp1c  6263  addccan2nc  6266  nnc3n3p1  6279