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

Theorem mp3an2 1440
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 1110 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 697 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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  df-3an 1081
This theorem is referenced by:  mp3anl2  1447  tz7.7  6210  ordin  6214  onfr  6223  wfrlem14  7957  wfrlem17  7960  tfrlem11  8013  epfrs  9161  zorng  9914  tsk2  10175  tskcard  10191  gruina  10228  muladd11  10798  00id  10803  ltaddneg  10843  negsub  10922  subneg  10923  muleqadd  11272  diveq1  11319  conjmul  11345  recp1lt1  11526  nnsub  11669  addltmul  11861  nnunb  11881  zltp1le  12020  gtndiv  12047  eluzp1m1  12256  zbtwnre  12334  rebtwnz  12335  xnn0le2is012  12627  supxrbnd  12709  divelunit  12868  fznatpl1  12949  flbi2  13175  fldiv  13216  modid  13252  modm1p1mod0  13278  fzen2  13325  nn0ennn  13335  seqshft2  13384  seqf1olem1  13397  ser1const  13414  sq01  13574  expnbnd  13581  faclbnd3  13640  faclbnd5  13646  hashunsng  13741  hashunsngx  13742  hashxplem  13782  ccatrid  13929  ccats1val1  13969  ccat2s1fst  13988  sgnn  14441  sqrlem2  14591  sqrlem7  14596  leabs  14647  abs2dif  14680  cvgrat  15227  cos2t  15519  sin01gt0  15531  cos01gt0  15532  demoivre  15541  demoivreALT  15542  rpnnen2lem5  15559  rpnnen2lem12  15566  omeo  15703  gcd0id  15855  sqgcd  15897  isprm3  16015  eulerthlem2  16107  pczpre  16172  pcrec  16183  ressress  16550  mulgm1  18186  unitgrpid  19348  mdet0pr  21129  m2detleib  21168  cmpcov2  21926  ufileu  22455  tgpconncompeqg  22647  itg2ge0  24263  mdegldg  24587  abssinper  25033  ppiub  25707  chtub  25715  bposlem2  25788  lgs1  25844  colinearalglem4  26622  axsegconlem1  26630  axpaschlem  26653  axcontlem2  26678  axcontlem4  26680  axcontlem7  26683  axcontlem8  26684  funvtxval  26730  funiedgval  26731  vc0  28278  vcm  28280  nvmval2  28347  nvmf  28349  nvmdi  28352  nvnegneg  28353  nvpncan2  28357  nvaddsub4  28361  nvm1  28369  nvdif  28370  nvpi  28371  nvz0  28372  nvmtri  28375  nvabs  28376  nvge0  28377  imsmetlem  28394  4ipval2  28412  ipval3  28413  ipidsq  28414  dipcj  28418  sspmval  28437  ipasslem1  28535  ipasslem2  28536  dipsubdir  28552  hvsubdistr1  28753  shsubcl  28924  shsel3  29019  shunssi  29072  hosubdi  29512  lnopmi  29704  nmophmi  29735  nmopcoi  29799  opsqrlem6  29849  hstle  29934  hst0  29937  mdsl2i  30026  superpos  30058  dmdbr5ati  30126  f1rnen  30302  resvsca  30830  pthhashvtx  32271  cvmliftphtlem  32461  topdifinffinlem  34510  finixpnum  34758  tan2h  34765  poimirlem3  34776  poimirlem4  34777  poimirlem7  34780  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem24  34797  poimirlem28  34801  mblfinlem2  34811  mblfinlem4  34813  ismblfin  34814  el3v2  35374  atlatle  36336  pmaple  36777  dihglblem2N  38310  expgcd  39061  elnnrabdioph  39282  rabren3dioph  39290  zindbi  39421  expgrowth  40544  binomcxplemnotnn0  40565  trelpss  40664  etransc  42445  mogoldbb  43827  pgrple2abl  44341  aacllem  44830
  Copyright terms: Public domain W3C validator