Theorem biimpd 198

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

Hypothesis

Ref	Expression
biimpd.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
biimpd	⊢ (φ → (ψ → χ))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		bi1 178	. 2 ⊢ ((ψ ↔ χ) → (ψ → χ))
3	1, 2	syl 15	1 ⊢ (φ → (ψ → χ))

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  2775  ceqsalg  2883  vtoclf  2908  vtocl2  2910  vtocl3  2911  spcdv  2937  rspcdv  2958  elabgt  2982  sbeqalb  3098  ssunsn2  3865  opkthg  4131  iotaval  4350  nnsucelr  4428  tfin11  4493  vfinspss  4551  0cnelphi  4597  iss  5000  tz6.12-1  5344  chfnrn  5399  elpreima  5407  ffnfv  5427  f1elima  5474  ndmovg  5613  enmap2lem3  6065  enmap1lem3  6071  enprmaplem3  6078  enprmaplem5  6080  nnltp1c  6262  addccan2nc  6265  nnc3n3p1  6278