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  2538  3netr3d  2542  rexlimd2  2736  ceqsalt  2881  vtoclgft  2905  vtoclegft  2926  eueq2  3010  sbceq1dd  3052  csbexg  3146  csbiedf  3173  sseqtrd  3307  3sstr3d  3313  ifbothda  3692  elimdhyp  3715  snssd  3853  dfnfc2  3909  opkth1g  4130  iota4  4357  findsd  4410  ltfintri  4466  t1csfin1c  4545  vfintle  4546  vfin1cltv  4547  vfinspclt  4552  breqtrd  4663  3brtr3d  4668  fssres2  5239  feu  5242  f1orescnv  5301  resdif  5306  fimacnv  5411  fsn2  5434  isoini2  5498  clos1is  5881  erthi  5970  mapsn  6026  enmap2lem5  6067  enmap1lem5  6073  enprmaplem5  6080  eqncg  6126  ceclr  6187  ceclnn1  6189  nc0suc  6217  te0c  6237  nmembers1lem3  6270  spacis  6288  nchoicelem5  6293  nchoicelem17  6305  nchoicelem19  6307  nchoice  6308  fnfreclem3  6319