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  2535  3netr4d  2544  eqsstrd  3306  3sstr4d  3315  lefinaddc  4451  nulge  4457  ltfinp1  4463  tfinprop  4490  sucevenodd  4511  sucoddeven  4512  sfintfin  4533  eqbrtrd  4660  3brtr4d  4670  eqfnfvd  5396  fvimacnvi  5403  fconst2g  5453  f1ofveu  5481  f1od  5727  brtxp  5784  trrd  5926  refrd  5927  antird  5929  connexrd  5931  iserd  5943  enmap2lem5  6068  enmap1lem5  6074  enprmaplem5  6081  nenpw1pwlem2  6086  pw1eltc  6163  ce0nnuli  6179  ce0  6191  lecidg  6197  lec0cg  6199  lecncvg  6200  addlec  6209  nmembers1lem3  6271  spacis  6289  nchoicelem17  6306  dmfrec  6317  frec0  6322  frecsuc  6323