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

Theorem mp3an2 1410
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 1263 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 716 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  mp3anl2  1417  tz7.7  5737  ordin  5741  onfr  5751  wfrlem14  7413  wfrlem17  7416  tfrlem11  7469  epfrs  8592  zorng  9311  tsk2  9572  tskcard  9588  gruina  9625  muladd11  10191  00id  10196  ltaddneg  10236  negsub  10314  subneg  10315  muleqadd  10656  diveq1  10703  conjmul  10727  recp1lt1  10906  nnsub  11044  addltmul  11253  nnunb  11273  zltp1le  11412  gtndiv  11439  eluzp1m1  11696  zbtwnre  11771  rebtwnz  11772  xnn0le2is012  12061  supxrbnd  12143  divelunit  12299  fznatpl1  12380  flbi2  12601  fldiv  12642  modid  12678  modm1p1mod0  12704  fzen2  12751  nn0ennn  12761  seqshft2  12810  seqf1olem1  12823  ser1const  12840  sq01  12969  expnbnd  12976  faclbnd3  13062  faclbnd5  13068  hashunsng  13164  hashxplem  13203  ccatrid  13353  sgnn  13815  sqrlem2  13965  sqrlem7  13970  leabs  14020  abs2dif  14053  cvgrat  14596  cos2t  14889  sin01gt0  14901  cos01gt0  14902  demoivre  14911  demoivreALT  14912  znnenlem  14921  rpnnen2lem5  14928  rpnnen2lem12  14935  omeo  15071  gcd0id  15221  sqgcd  15259  isprm3  15377  eulerthlem2  15468  pczpre  15533  pcrec  15544  ressress  15919  mulgm1  17543  unitgrpid  18650  mdet0pr  20379  m2detleib  20418  cmpcov2  21174  ufileu  21704  tgpconncompeqg  21896  itg2ge0  23483  mdegldg  23807  abssinper  24251  ppiub  24910  chtub  24918  bposlem2  24991  lgs1  25047  colinearalglem4  25770  axsegconlem1  25778  axpaschlem  25801  axcontlem2  25826  axcontlem4  25828  axcontlem7  25831  axcontlem8  25832  funvtxval  25886  funiedgval  25887  vc0  27399  vcm  27401  nvmval2  27468  nvmf  27470  nvmdi  27473  nvnegneg  27474  nvpncan2  27478  nvaddsub4  27482  nvm1  27490  nvdif  27491  nvpi  27492  nvz0  27493  nvmtri  27496  nvabs  27497  nvge0  27498  imsmetlem  27515  4ipval2  27533  ipval3  27534  ipidsq  27535  dipcj  27539  sspmval  27558  ipasslem1  27656  ipasslem2  27657  dipsubdir  27673  hvsubdistr1  27876  shsubcl  28047  shsel3  28144  shunssi  28197  hosubdi  28637  lnopmi  28829  nmophmi  28860  nmopcoi  28924  opsqrlem6  28974  hstle  29059  hst0  29062  mdsl2i  29151  superpos  29183  dmdbr5ati  29251  resvsca  29804  cvmliftphtlem  31273  topdifinffinlem  33166  finixpnum  33365  tan2h  33372  poimirlem3  33383  poimirlem4  33384  poimirlem7  33387  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem24  33404  poimirlem28  33408  mblfinlem2  33418  mblfinlem4  33420  ismblfin  33421  atlatle  34426  pmaple  34866  dihglblem2N  36402  elnnrabdioph  37190  rabren3dioph  37198  zindbi  37330  expgrowth  38354  binomcxplemnotnn0  38375  trelpss  38479  etransc  40263  mogoldbb  41438  pgrple2abl  41911  aacllem  42312
  Copyright terms: Public domain W3C validator