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

Theorem mpanl2 712
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 562 . 2 (𝜑 → (𝜑𝜓))
3 mpanl2.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 486 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  mpanr1  714  mp3an2  1403  reuss  3866  tfrlem11  7348  tfr3  7359  oe0  7466  dif1en  8055  indpi  9585  map2psrpr  9787  axcnre  9841  muleqadd  10520  divdiv2  10586  addltmul  11115  frnnn0supp  11196  supxrpnf  11976  supxrunb1  11977  supxrunb2  11978  iimulcl  22475  numclwwlkovf2ex  26379  eigposi  27885  nmopadjlem  28138  nmopcoadji  28150  opsqrlem6  28194  hstrbi  28315  sgncl  29733  poimirlem3  32385  av-numclwwlkovf2ex  41519  aacllem  42319
  Copyright terms: Public domain W3C validator