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 ⊢ (𝜃 → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ralxfr2d  5383  ovmpt4g  7566  ov3  7582  omeulem2  8574  domtriomlem  10441  nsmallnq  10977  bposlem1  27499  pntrsumbnd  27781  elntg2  29390  mptsnunlem  38041  poimirlem27  38355  refressn  39240  frege92  44739  nzss  45085  modelaxreplem1  45745  ormklocald  47648  setis  50533