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  5380  ovmpt4g  7554  ov3  7570  omeulem2  8595  domtriomlem  10456  nsmallnq  10991  bposlem1  27247  pntrsumbnd  27529  elntg2  28964  mptsnunlem  37356  poimirlem27  37671  refressn  38461  frege92  43979  nzss  44341  modelaxreplem1  45003  ormklocald  46903  setis  49562