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

Theorem mpanl2 700
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 526 . 2 (𝜑 → (𝜑𝜓))
3 mpanl2.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 581 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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  df-an 398
This theorem is referenced by:  mpanr1  702  mp3an2  1450  reuss  4275  tfrlem11  8327  tfr3  8338  oe0  8461  unfi  9075  dif1ennnALT  9180  indpi  10802  map2psrpr  11005  axcnre  11059  muleqadd  11758  divdiv2  11826  addltmul  12348  supxrpnf  13192  supxrunb1  13193  supxrunb2  13194  iimulcl  24252  clwwlknonex2lem2  28881  nmopadjlem  30860  nmopcoadji  30872  opsqrlem6  30916  hstrbi  31037  sgncl  32942  poimirlem3  36013  dflim5  41564  aacllem  47143
  Copyright terms: Public domain W3C validator