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

Theorem mpanr12 717
Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
Hypotheses
Ref Expression
mpanr12.1 𝜓
mpanr12.2 𝜒
mpanr12.3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
mpanr12 (𝜑𝜃)

Proof of Theorem mpanr12
StepHypRef Expression
1 mpanr12.2 . 2 𝜒
2 mpanr12.1 . . 3 𝜓
3 mpanr12.3 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3mpanr1 715 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 703 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 196  df-an 385
This theorem is referenced by:  wfisg  5632  2dom  7915  limensuci  8021  phplem4  8027  unfi  8112  fiint  8122  cdaen  8878  isfin1-3  9091  prlem934  9734  0idsr  9797  1idsr  9798  00sr  9799  addresr  9838  mulresr  9839  reclt1  10797  crne0  10890  nominpos  11146  expnass  12832  faclbnd2  12940  crim  13703  sqrlem1  13831  sqrlem7  13837  sqrt00  13852  sqreulem  13947  mulcn2  14174  ege2le3  14659  sin02gt0  14761  opoe  14925  oddprm  15353  pythagtriplem2  15360  pythagtriplem3  15361  pythagtriplem16  15373  pythagtrip  15377  pc1  15398  prmlem0  15650  acsfn0  16144  mgpress  18323  abvneg  18657  pmatcollpw3  20408  leordtval2  20826  txswaphmeo  21418  iccntr  22432  dvlipcn  23561  sinq34lt0t  24065  cosordlem  24081  efif1olem3  24094  lgamgulmlem2  24556  basellem3  24609  ppiub  24729  bposlem9  24817  lgsne0  24860  lgsdinn0  24870  chebbnd1  24961  constr1trl  26118  constr2trl  26129  usgrcyclnl2  26169  4cycl4dv  26195  2spontn0vne  26414  eupath2lem3  26506  mayete3i  27971  lnop0  28209  nmcexi  28269  nmoptrii  28337  nmopcoadji  28344  hstle1  28469  hst0  28476  strlem5  28498  jplem1  28511  cnvoprab  28886  subfacp1lem5  30420  frinsg  30986  limsucncmpi  31614  matunitlindflem1  32575  poimirlem15  32594  dvasin  32666  fdc  32711  eldioph3b  36346  eupth2lem3lem4  41399  sinhpcosh  42280
  Copyright terms: Public domain W3C validator