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

Theorem mp3an2 1560
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 1111 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 681 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  mp3anl2  1567  tz7.7  5892  ordin  5896  onfr  5906  wfrlem14  7581  wfrlem17  7584  tfrlem11  7637  epfrs  8771  zorng  9528  tsk2  9789  tskcard  9805  gruina  9842  muladd11  10408  00id  10413  ltaddneg  10453  negsub  10531  subneg  10532  muleqadd  10873  diveq1  10920  conjmul  10944  recp1lt1  11123  nnsub  11261  addltmul  11470  nnunb  11490  zltp1le  11629  gtndiv  11656  eluzp1m1  11912  zbtwnre  11989  rebtwnz  11990  xnn0le2is012  12281  supxrbnd  12363  divelunit  12521  fznatpl1  12602  flbi2  12826  fldiv  12867  modid  12903  modm1p1mod0  12929  fzen2  12976  nn0ennn  12986  seqshft2  13034  seqf1olem1  13047  ser1const  13064  sq01  13193  expnbnd  13200  faclbnd3  13283  faclbnd5  13289  hashunsng  13383  hashxplem  13422  ccatrid  13569  sgnn  14042  sqrlem2  14192  sqrlem7  14197  leabs  14247  abs2dif  14280  cvgrat  14822  cos2t  15114  sin01gt0  15126  cos01gt0  15127  demoivre  15136  demoivreALT  15137  znnenlem  15146  rpnnen2lem5  15153  rpnnen2lem12  15160  omeo  15298  gcd0id  15448  sqgcd  15486  isprm3  15603  eulerthlem2  15694  pczpre  15759  pcrec  15770  ressress  16146  mulgm1  17770  unitgrpid  18877  mdet0pr  20616  m2detleib  20655  cmpcov2  21414  ufileu  21943  tgpconncompeqg  22135  itg2ge0  23722  mdegldg  24046  abssinper  24491  ppiub  25150  chtub  25158  bposlem2  25231  lgs1  25287  colinearalglem4  26010  axsegconlem1  26018  axpaschlem  26041  axcontlem2  26066  axcontlem4  26068  axcontlem7  26071  axcontlem8  26072  funvtxval  26126  funiedgval  26127  vc0  27769  vcm  27771  nvmval2  27838  nvmf  27840  nvmdi  27843  nvnegneg  27844  nvpncan2  27848  nvaddsub4  27852  nvm1  27860  nvdif  27861  nvpi  27862  nvz0  27863  nvmtri  27866  nvabs  27867  nvge0  27868  imsmetlem  27885  4ipval2  27903  ipval3  27904  ipidsq  27905  dipcj  27909  sspmval  27928  ipasslem1  28026  ipasslem2  28027  dipsubdir  28043  hvsubdistr1  28246  shsubcl  28417  shsel3  28514  shunssi  28567  hosubdi  29007  lnopmi  29199  nmophmi  29230  nmopcoi  29294  opsqrlem6  29344  hstle  29429  hst0  29432  mdsl2i  29521  superpos  29553  dmdbr5ati  29621  resvsca  30170  cvmliftphtlem  31637  topdifinffinlem  33532  finixpnum  33727  tan2h  33734  poimirlem3  33745  poimirlem4  33746  poimirlem7  33749  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem24  33766  poimirlem28  33770  mblfinlem2  33780  mblfinlem4  33782  ismblfin  33783  el3v2  34334  atlatle  35129  pmaple  35569  dihglblem2N  37104  elnnrabdioph  37897  rabren3dioph  37905  zindbi  38037  expgrowth  39060  binomcxplemnotnn0  39081  trelpss  39184  etransc  41017  mogoldbb  42201  pgrple2abl  42674  aacllem  43078
  Copyright terms: Public domain W3C validator