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

Theorem mpanl2 701
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
mpanl2.1 𝜓
mpanl2.2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
mpanl2 ((𝜑𝜒) → 𝜃)

Proof of Theorem mpanl2
StepHypRef Expression
1 mpanl2.1 . . 3 𝜓
21jctr 528 . 2 (𝜑 → (𝜑𝜓))
3 mpanl2.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 583 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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  df-an 400
This theorem is referenced by:  mpanr1  703  mp3an2  1451  reuss  4231  tfrlem11  8124  tfr3  8135  oe0  8249  unfi  8850  dif1enALT  8907  indpi  10521  map2psrpr  10724  axcnre  10778  muleqadd  11476  divdiv2  11544  addltmul  12066  supxrpnf  12908  supxrunb1  12909  supxrunb2  12910  iimulcl  23834  clwwlknonex2lem2  28191  nmopadjlem  30170  nmopcoadji  30182  opsqrlem6  30226  hstrbi  30347  sgncl  32217  poimirlem3  35517  aacllem  46176
  Copyright terms: Public domain W3C validator