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

Theorem mpanr12 701
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 699 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 687 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:  wfisg  6176  2dom  8570  limensuci  8681  phplem4  8687  unfi  8773  fiint  8783  djuen  9583  isfin1-3  9796  prlem934  10443  0idsr  10507  1idsr  10508  00sr  10509  addresr  10548  mulresr  10549  reclt1  11523  crne0  11619  nominpos  11862  expnass  13558  faclbnd2  13639  crim  14462  sqrlem1  14590  sqrlem7  14596  sqrt00  14611  sqreulem  14707  mulcn2  14940  ege2le3  15431  sin02gt0  15533  opoe  15700  oddprm  16135  pythagtriplem2  16142  pythagtriplem3  16143  pythagtriplem16  16155  pythagtrip  16159  pc1  16180  prmlem0  16427  acsfn0  16919  mgpress  19179  abvneg  19534  pmatcollpw3  21320  leordtval2  21748  txswaphmeo  22341  iccntr  23356  dvlipcn  24518  sinq34lt0t  25022  cosordlem  25042  efif1olem3  25055  lgamgulmlem2  25534  basellem3  25587  ppiub  25707  bposlem9  25795  lgsne0  25838  lgsdinn0  25848  chebbnd1  25975  eupth2lem3lem4  27937  mayete3i  29432  lnop0  29670  nmcexi  29730  nmoptrii  29798  nmopcoadji  29805  hstle1  29930  hst0  29937  strlem5  29959  jplem1  29972  cnvoprabOLD  30382  subfacp1lem5  32328  frinsg  32984  limsucncmpi  33690  matunitlindflem1  34769  poimirlem15  34788  dvasin  34859  fdc  34901  eldioph3b  39240  or2expropbi  43146  ich2exprop  43510  sprsymrelfolem2  43532  sinhpcosh  44767
  Copyright terms: Public domain W3C validator