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

Theorem mp3an2 1403
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an2.1 𝜓
mp3an2.2 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an2 ((𝜑𝜒) → 𝜃)

Proof of Theorem mp3an2
StepHypRef Expression
1 mp3an2.1 . 2 𝜓
2 mp3an2.2 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expa 1256 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 712 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  mp3anl2  1410  tz7.7  5652  ordin  5656  onfr  5666  wfrlem14  7292  wfrlem17  7295  tfrlem11  7348  epfrs  8467  zorng  9186  tsk2  9443  tskcard  9459  gruina  9496  muladd11  10057  00id  10062  ltaddneg  10102  negsub  10180  subneg  10181  muleqadd  10520  diveq1  10567  conjmul  10591  recp1lt1  10770  nnsub  10906  addltmul  11115  nnunb  11135  zltp1le  11260  gtndiv  11286  eluzp1m1  11543  zbtwnre  11618  rebtwnz  11619  supxrbnd  11986  divelunit  12141  fznatpl1  12220  flbi2  12435  fldiv  12476  modid  12512  modm1p1mod0  12538  fzen2  12585  nn0ennn  12595  seqshft2  12644  seqf1olem1  12657  ser1const  12674  sq01  12803  expnbnd  12810  faclbnd3  12896  faclbnd5  12902  hashunsng  12994  hashxplem  13032  ccatrid  13169  sgnn  13628  sqrlem2  13778  sqrlem7  13783  leabs  13833  abs2dif  13866  cvgrat  14400  cos2t  14693  sin01gt0  14705  cos01gt0  14706  demoivre  14715  demoivreALT  14716  znnenlem  14725  rpnnen2lem5  14732  rpnnen2lem12  14739  omeo  14874  gcd0id  15024  sqgcd  15062  isprm3  15180  eulerthlem2  15271  pczpre  15336  pcrec  15347  ressress  15711  mulgm1  17331  unitgrpid  18438  mdet0pr  20159  m2detleib  20198  cmpcov2  20945  ufileu  21475  tgpconcompeqg  21667  itg2ge0  23225  mdegldg  23547  abssinper  23991  ppiub  24646  chtub  24654  bposlem2  24727  lgs1  24783  colinearalglem4  25507  axsegconlem1  25515  axpaschlem  25538  axcontlem2  25563  axcontlem4  25565  axcontlem7  25568  axcontlem8  25569  constr2spthlem1  25890  2pthon3v  25900  el2spthonot  26163  el2spthonot0  26164  frg2woteq  26353  vc0  26590  vcm  26592  vcnegsubdi2OLD  26596  vcsub4OLD  26597  nvmval2  26668  nvzs  26670  nvmf  26671  nvmdi  26675  nvnegneg  26676  nvsubadd  26680  nvpncan2  26681  nvaddsub4  26686  nvnncan  26688  nvm1  26697  nvdif  26698  nvpi  26699  nvz0  26701  nvmtri  26704  nvabs  26706  nvge0  26707  imsmetlem  26726  4ipval2  26748  ipval3  26749  ipidsq  26753  dipcj  26757  sspmval  26776  ipasslem1  26876  ipasslem2  26877  dipsubdir  26893  hvsubdistr1  27096  shsubcl  27267  shsel3  27364  shunssi  27417  hosubdi  27857  lnopmi  28049  nmophmi  28080  nmopcoi  28144  opsqrlem6  28194  hstle  28279  hst0  28282  mdsl2i  28371  superpos  28403  dmdbr5ati  28471  resvsca  28967  cvmliftphtlem  30359  topdifinffinlem  32167  finixpnum  32360  tan2h  32367  poimirlem3  32378  poimirlem4  32379  poimirlem7  32382  poimirlem16  32391  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem24  32399  poimirlem28  32403  mblfinlem2  32413  mblfinlem4  32415  ismblfin  32416  atlatle  33421  pmaple  33861  dihglblem2N  35397  elnnrabdioph  36185  rabren3dioph  36193  zindbi  36325  expgrowth  37352  binomcxplemnotnn0  37373  trelpss  37476  etransc  38973  upgredg  40365  01wlk  41279  0Trl  41285  0pth-av  41288  0spth-av  41289  0Crct  41295  0Cycl  41296  pgrple2abl  41935  aacllem  42312
  Copyright terms: Public domain W3C validator