Theorem mpbidi 244

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 232	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	sylcom 31	1 ⊢ (𝜃 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ralxfr2d  5382  ovmpt4g  7558  ov3  7574  omeulem2  8567  domtriomlem  10425  nsmallnq  10961  bposlem1  27413  pntrsumbnd  27695  elntg2  29275  mptsnunlem  37871  poimirlem27  38185  refressn  39071  frege92  44572  nzss  44918  modelaxreplem1  45578  ormklocald  47481  setis  50360