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

Theorem mpanr2 700
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 525 . 2 (𝜓 → (𝜓𝜒))
3 mpanr2.2 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3sylan2 592 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  fvreseq1  6681  op1steq  7596  fpmg  8289  pmresg  8291  pw2f1o  8476  pm54.43  9282  dfac2b  9409  ttukeylem6  9789  gruina  10093  muleqadd  11138  divdiv1  11205  addltmul  11727  elfzp1b  12838  elfzm1b  12839  expp1z  13332  expm1  13333  oddvdsnn0  18407  efgi0  18577  efgi1  18578  fiinbas  21248  opnneissb  21410  fclscf  22321  blssec  22732  iimulcl  23228  itg2lr  24018  blocnilem  28268  lnopmul  29431  opsqrlem6  29609  gsumle  30490  gsumvsca1  30493  gsumvsca2  30494  locfinreflem  30717  fvray  33213  fvline  33216  fneref  33309  poimirlem3  34447  poimirlem16  34460  fdc  34573  linepmap  36463  rmyeq0  39056
  Copyright terms: Public domain W3C validator