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

Theorem mpanl2 681
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 514 . 2 (𝜑 → (𝜑𝜓))
3 mpanl2.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 569 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 197  df-an 383
This theorem is referenced by:  mpanr1  683  mp3an2  1560  reuss  4056  tfrlem11  7637  tfr3  7648  oe0  7756  dif1en  8349  indpi  9931  map2psrpr  10133  axcnre  10187  muleqadd  10873  divdiv2  10939  addltmul  11470  frnnn0supp  11551  supxrpnf  12353  supxrunb1  12354  supxrunb2  12355  iimulcl  22956  clwwlknonex2lem2  27284  nmopadjlem  29288  nmopcoadji  29300  opsqrlem6  29344  hstrbi  29465  sgncl  30940  poimirlem3  33745  aacllem  43078
  Copyright terms: Public domain W3C validator