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

Theorem mp3an2 1566
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 1140 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 684 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  mp3anl2  1573  tz7.7  5959  ordin  5963  onfr  5973  wfrlem14  7661  wfrlem17  7664  tfrlem11  7717  epfrs  8851  zorng  9608  tsk2  9869  tskcard  9885  gruina  9922  muladd11  10488  00id  10493  ltaddneg  10533  negsub  10611  subneg  10612  muleqadd  10953  diveq1  11000  conjmul  11024  recp1lt1  11203  nnsub  11341  addltmul  11531  nnunb  11551  zltp1le  11689  gtndiv  11716  eluzp1m1  11924  zbtwnre  12001  rebtwnz  12002  xnn0le2is012  12290  supxrbnd  12372  divelunit  12533  fznatpl1  12614  flbi2  12838  fldiv  12879  modid  12915  modm1p1mod0  12941  fzen2  12988  nn0ennn  12998  seqshft2  13046  seqf1olem1  13059  ser1const  13076  sq01  13205  expnbnd  13212  faclbnd3  13295  faclbnd5  13301  hashunsng  13395  hashxplem  13433  ccatrid  13580  sgnn  14053  sqrlem2  14203  sqrlem7  14208  leabs  14258  abs2dif  14291  cvgrat  14832  cos2t  15124  sin01gt0  15136  cos01gt0  15137  demoivre  15146  demoivreALT  15147  znnenlemOLD  15156  rpnnen2lem5  15163  rpnnen2lem12  15170  omeo  15306  gcd0id  15455  sqgcd  15493  isprm3  15610  eulerthlem2  15700  pczpre  15765  pcrec  15776  ressress  16146  mulgm1  17762  unitgrpid  18867  mdet0pr  20605  m2detleib  20644  cmpcov2  21403  ufileu  21932  tgpconncompeqg  22124  itg2ge0  23712  mdegldg  24036  abssinper  24481  ppiub  25139  chtub  25147  bposlem2  25220  lgs1  25276  colinearalglem4  25999  axsegconlem1  26007  axpaschlem  26030  axcontlem2  26055  axcontlem4  26057  axcontlem7  26060  axcontlem8  26061  funvtxval  26115  funiedgval  26116  vc0  27754  vcm  27756  nvmval2  27823  nvmf  27825  nvmdi  27828  nvnegneg  27829  nvpncan2  27833  nvaddsub4  27837  nvm1  27845  nvdif  27846  nvpi  27847  nvz0  27848  nvmtri  27851  nvabs  27852  nvge0  27853  imsmetlem  27870  4ipval2  27888  ipval3  27889  ipidsq  27890  dipcj  27894  sspmval  27913  ipasslem1  28011  ipasslem2  28012  dipsubdir  28028  hvsubdistr1  28231  shsubcl  28402  shsel3  28499  shunssi  28552  hosubdi  28992  lnopmi  29184  nmophmi  29215  nmopcoi  29279  opsqrlem6  29329  hstle  29414  hst0  29417  mdsl2i  29506  superpos  29538  dmdbr5ati  29606  resvsca  30152  cvmliftphtlem  31619  topdifinffinlem  33508  finixpnum  33704  tan2h  33711  poimirlem3  33722  poimirlem4  33723  poimirlem7  33726  poimirlem16  33735  poimirlem17  33736  poimirlem19  33738  poimirlem20  33739  poimirlem24  33743  poimirlem28  33747  mblfinlem2  33757  mblfinlem4  33759  ismblfin  33760  el3v2  34307  atlatle  35097  pmaple  35538  dihglblem2N  37072  elnnrabdioph  37870  rabren3dioph  37878  zindbi  38009  expgrowth  39031  binomcxplemnotnn0  39052  trelpss  39154  etransc  40976  mogoldbb  42245  pgrple2abl  42711  aacllem  43115
  Copyright terms: Public domain W3C validator