Theorem mpbidi 241

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

Hypotheses

Ref	Expression
mpbidi.min	⊢ (𝜃 → (𝜑 → 𝜓))
mpbidi.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbidi	⊢ (𝜃 → (𝜑 → 𝜒))

Proof of Theorem mpbidi

Step	Hyp	Ref	Expression
1		mpbidi.min	. 2 ⊢ (𝜃 → (𝜑 → 𝜓))
2		mpbidi.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 229	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	sylcom 30	1 ⊢ (𝜃 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  ralxfr2d  5356  ovmpt4g  7507  ov3  7523  omeulem2  8512  domtriomlem  10356  nsmallnq  10892  bposlem1  27255  pntrsumbnd  27537  elntg2  29041  mptsnunlem  37514  poimirlem27  37819  refressn  38705  frege92  44232  nzss  44594  modelaxreplem1  45255  ormklocald  47154  setis  49979