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

Theorem mpanl2 717
 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 564 . 2 (𝜑 → (𝜑𝜓))
3 mpanl2.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 487 1 ((𝜑𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  mpanr1  719  mp3an2  1452  reuss  3941  tfrlem11  7529  tfr3  7540  oe0  7647  dif1en  8234  indpi  9767  map2psrpr  9969  axcnre  10023  muleqadd  10709  divdiv2  10775  addltmul  11306  frnnn0supp  11387  supxrpnf  12186  supxrunb1  12187  supxrunb2  12188  iimulcl  22783  clwwlknonex2lem2  27083  eigposi  28823  nmopadjlem  29076  nmopcoadji  29088  opsqrlem6  29132  hstrbi  29253  sgncl  30728  poimirlem3  33542  aacllem  42875
 Copyright terms: Public domain W3C validator