Theorem mpbird 223

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

Hypotheses

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

Assertion

Ref	Expression
mpbird	⊢ (φ → ψ)

Proof of Theorem mpbird

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 ⊢ (φ → χ)
2		mpbird.maj	. . 3 ⊢ (φ → (ψ ↔ χ))
3	2	biimprd 214	. 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:  mpbiri  224  mpbir2and  888  mpbir3and  1135  eqeltrd  2427  eqnetrd  2534  3netr4d  2543  eqsstrd  3305  3sstr4d  3314  lefinaddc  4450  nulge  4456  ltfinp1  4462  tfinprop  4489  sucevenodd  4510  sucoddeven  4511  sfintfin  4532  eqbrtrd  4659  3brtr4d  4669  eqfnfvd  5395  fvimacnvi  5402  fconst2g  5452  f1ofveu  5480  f1od  5726  brtxp  5783  trrd  5925  refrd  5926  antird  5928  connexrd  5930  iserd  5942  enmap2lem5  6067  enmap1lem5  6073  enprmaplem5  6080  nenpw1pwlem2  6085  pw1eltc  6162  ce0nnuli  6178  ce0  6190  lecidg  6196  lec0cg  6198  lecncvg  6199  addlec  6208  nmembers1lem3  6270  spacis  6288  nchoicelem17  6305  dmfrec  6316  frec0  6321  frecsuc  6322