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

Theorem mpanl2 716
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 488 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  mpanr1  718  mp3an2  1409  reuss  3890  tfrlem11  7444  tfr3  7455  oe0  7562  dif1en  8153  indpi  9689  map2psrpr  9891  axcnre  9945  muleqadd  10631  divdiv2  10697  addltmul  11228  frnnn0supp  11309  supxrpnf  12107  supxrunb1  12108  supxrunb2  12109  iimulcl  22676  numclwwlkovf2ex  27109  eigposi  28583  nmopadjlem  28836  nmopcoadji  28848  opsqrlem6  28892  hstrbi  29013  sgncl  30423  poimirlem3  33083  aacllem  41880
  Copyright terms: Public domain W3C validator