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  5408  ovmpt4g  7557  ov3  7572  omeulem2  8585  domtriomlem  10439  nsmallnq  10974  bposlem1  27011  pntrsumbnd  27293  elntg2  28498  mptsnunlem  36522  poimirlem27  36818  refressn  37616  frege92  43008  nzss  43378  setis  47831
  Copyright terms: Public domain W3C validator