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

Theorem mpanr2 722
 Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpanr2.1 𝜒
mpanr2.2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
mpanr2 ((𝜑𝜓) → 𝜃)

Proof of Theorem mpanr2
StepHypRef Expression
1 mpanr2.1 . . 3 𝜒
21jctr 566 . 2 (𝜓 → (𝜓𝜒))
3 mpanr2.2 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3sylan2 492 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:  fvreseq1  6469  op1steq  7365  fpmg  8037  pmresg  8039  pw2f1o  8218  pm54.43  8987  dfac2b  9114  dfac2OLD  9116  ttukeylem6  9499  gruina  9803  muleqadd  10834  divdiv1  10899  addltmul  11431  elfzp1b  12581  elfzm1b  12582  expp1z  13074  expm1  13075  oddvdsnn0  18134  efgi0  18304  efgi1  18305  fiinbas  20929  opnneissb  21091  fclscf  22001  blssec  22412  iimulcl  22908  itg2lr  23667  blocnilem  27939  lnopmul  29106  opsqrlem6  29284  gsumle  30059  gsumvsca1  30062  gsumvsca2  30063  locfinreflem  30187  fvray  32525  fvline  32528  fneref  32622  poimirlem3  33694  poimirlem16  33707  fdc  33823  linepmap  35533  rmyeq0  37991
 Copyright terms: Public domain W3C validator