Theorem mpbid 201

Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbid.min	⊢ (φ → ψ)
mpbid.maj	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
mpbid	⊢ (φ → χ)

Proof of Theorem mpbid

Step	Hyp	Ref	Expression
1		mpbid.min	. 2 ⊢ (φ → ψ)
2		mpbid.maj	. . 3 ⊢ (φ → (ψ ↔ χ))
3	2	biimpd 198	. 2 ⊢ (φ → (ψ → χ))
4	1, 3	mpd 14	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:  mpbii  202  mpbi2and  887  dvelimdf  2082  ax11eq  2193  ax11el  2194  eqtrd  2385  eleqtrd  2429  neeqtrd  2539  3netr3d  2543  rexlimd2  2737  ceqsalt  2882  vtoclgft  2906  vtoclegft  2927  eueq2  3011  sbceq1dd  3053  csbexg  3147  csbiedf  3174  sseqtrd  3308  3sstr3d  3314  ifbothda  3693  elimdhyp  3716  snssd  3854  dfnfc2  3910  opkth1g  4131  iota4  4358  findsd  4411  ltfintri  4467  t1csfin1c  4546  vfintle  4547  vfin1cltv  4548  vfinspclt  4553  breqtrd  4664  3brtr3d  4669  fssres2  5240  feu  5243  f1orescnv  5302  resdif  5307  fimacnv  5412  fsn2  5435  isoini2  5499  clos1is  5882  erthi  5971  mapsn  6027  enmap2lem5  6068  enmap1lem5  6074  enprmaplem5  6081  eqncg  6127  ceclr  6188  ceclnn1  6190  nc0suc  6218  te0c  6238  nmembers1lem3  6271  spacis  6289  nchoicelem5  6294  nchoicelem17  6306  nchoicelem19  6308  nchoice  6309  fnfreclem3  6320