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

Theorem mpanr2 704
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 528 . 2 (𝜓 → (𝜓𝜒))
3 mpanr2.2 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3sylan2 596 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  fvreseq1  6859  op1steq  7805  fpmg  8549  pmresg  8551  pw2f1o  8750  pm54.43  9617  dfac2b  9744  ttukeylem6  10128  gruina  10432  muleqadd  11476  divdiv1  11543  addltmul  12066  elfzp1b  13189  elfzm1b  13190  expp1z  13684  expm1  13685  oddvdsnn0  18936  efgi0  19110  efgi1  19111  fiinbas  21849  opnneissb  22011  fclscf  22922  blssec  23333  iimulcl  23834  itg2lr  24628  blocnilem  28885  lnopmul  30048  opsqrlem6  30226  gsumle  31069  gsumvsca1  31198  gsumvsca2  31199  locfinreflem  31504  fvray  34180  fvline  34183  fneref  34276  poimirlem3  35517  poimirlem16  35530  fdc  35640  linepmap  37526  rmyeq0  40478
  Copyright terms: Public domain W3C validator