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

Theorem mpanr12 705
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 703 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 691 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  wfisgOLD  6375  f1ofvswap  7326  2dom  9070  limensuci  9193  phplem4OLD  9257  fiintOLD  9367  frinsg  9791  djuen  10210  isfin1-3  10426  prlem934  11073  0idsr  11137  1idsr  11138  00sr  11139  addresr  11178  mulresr  11179  reclt1  12163  crne0  12259  nominpos  12503  fvf1tp  13829  expnass  14247  faclbnd2  14330  crim  15154  01sqrexlem1  15281  01sqrexlem7  15287  sqrt00  15302  sqreulem  15398  mulcn2  15632  ege2le3  16126  sin02gt0  16228  opoe  16400  oddprm  16848  pythagtriplem2  16855  pythagtriplem3  16856  pythagtriplem16  16868  pythagtrip  16872  pc1  16893  prmlem0  17143  acsfn0  17703  mgpress  20147  abvneg  20827  pmatcollpw3  22790  leordtval2  23220  txswaphmeo  23813  iccntr  24843  dvlipcn  26033  sinq34lt0t  26551  cosordlem  26572  efif1olem3  26586  lgamgulmlem2  27073  basellem3  27126  ppiub  27248  bposlem9  27336  lgsne0  27379  lgsdinn0  27389  chebbnd1  27516  eupth2lem3lem4  30250  mayete3i  31747  lnop0  31985  nmcexi  32045  nmoptrii  32113  nmopcoadji  32120  hstle1  32245  hst0  32252  strlem5  32274  jplem1  32287  subfacp1lem5  35189  limsucncmpi  36446  matunitlindflem1  37623  poimirlem15  37642  dvasin  37711  fdc  37752  eldioph3b  42776  oaabsb  43307  tfsconcatfv2  43353  omssaxinf2  45005  or2expropbi  47046  ich2exprop  47458  sprsymrelfolem2  47480  clnbgrisubgrgrim  47900  sinhpcosh  49259
  Copyright terms: Public domain W3C validator