MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbidi Structured version   Visualization version   GIF version

Theorem mpbidi 240
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
StepHypRef Expression
1 mpbidi.min . 2 (𝜃 → (𝜑𝜓))
2 mpbidi.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 228 . 2 (𝜑 → (𝜓𝜒))
41, 3sylcom 30 1 (𝜃 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  ralxfr2d  5407  ovmpt4g  7557  ov3  7572  omeulem2  8585  domtriomlem  10439  nsmallnq  10974  bposlem1  27023  pntrsumbnd  27305  elntg2  28510  mptsnunlem  36522  poimirlem27  36818  refressn  37616  frege92  43008  nzss  43378  setis  47830
  Copyright terms: Public domain W3C validator