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

Theorem mp3an2 1446
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 1115 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 700 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  mp3anl2  1453  tz7.7  6189  ordin  6193  onfr  6202  wfrlem14  7955  wfrlem17  7958  tfrlem11  8011  epfrs  9161  zorng  9919  tsk2  10180  tskcard  10196  gruina  10233  muladd11  10803  00id  10808  ltaddneg  10848  negsub  10927  subneg  10928  muleqadd  11277  diveq1  11324  conjmul  11350  recp1lt1  11531  nnsub  11673  addltmul  11865  nnunb  11885  zltp1le  12024  gtndiv  12051  eluzp1m1  12260  zbtwnre  12338  rebtwnz  12339  xnn0le2is012  12631  supxrbnd  12713  divelunit  12876  fznatpl1  12960  flbi2  13186  fldiv  13227  modid  13263  modm1p1mod0  13289  fzen2  13336  nn0ennn  13346  seqshft2  13396  seqf1olem1  13409  ser1const  13426  sq01  13586  expnbnd  13593  faclbnd3  13652  faclbnd5  13658  hashunsng  13753  hashunsngx  13754  hashxplem  13794  ccatrid  13936  ccats1val1  13976  ccat2s1fst  13995  sgnn  14449  sqrlem2  14599  sqrlem7  14604  leabs  14655  abs2dif  14688  cvgrat  15235  cos2t  15527  sin01gt0  15539  cos01gt0  15540  demoivre  15549  demoivreALT  15550  rpnnen2lem5  15567  rpnnen2lem12  15574  omeo  15711  gcd0id  15861  sqgcd  15903  isprm3  16021  eulerthlem2  16113  pczpre  16178  pcrec  16189  ressress  16558  mulgm1  18244  unitgrpid  19419  mdet0pr  21201  m2detleib  21240  cmpcov2  21999  ufileu  22528  tgpconncompeqg  22721  itg2ge0  24343  mdegldg  24671  abssinper  25117  ppiub  25792  chtub  25800  bposlem2  25873  lgs1  25929  colinearalglem4  26707  axsegconlem1  26715  axpaschlem  26738  axcontlem2  26763  axcontlem4  26765  axcontlem7  26768  axcontlem8  26769  funvtxval  26815  funiedgval  26816  vc0  28361  vcm  28363  nvmval2  28430  nvmf  28432  nvmdi  28435  nvnegneg  28436  nvpncan2  28440  nvaddsub4  28444  nvm1  28452  nvdif  28453  nvpi  28454  nvz0  28455  nvmtri  28458  nvabs  28459  nvge0  28460  imsmetlem  28477  4ipval2  28495  ipval3  28496  ipidsq  28497  dipcj  28501  sspmval  28520  ipasslem1  28618  ipasslem2  28619  dipsubdir  28635  hvsubdistr1  28836  shsubcl  29007  shsel3  29102  shunssi  29155  hosubdi  29595  lnopmi  29787  nmophmi  29818  nmopcoi  29882  opsqrlem6  29932  hstle  30017  hst0  30020  mdsl2i  30109  superpos  30141  dmdbr5ati  30209  f1rnen  30392  resvsca  30958  pthhashvtx  32488  cvmliftphtlem  32678  topdifinffinlem  34765  finixpnum  35041  tan2h  35048  poimirlem3  35059  poimirlem4  35060  poimirlem7  35063  poimirlem16  35072  poimirlem17  35073  poimirlem19  35075  poimirlem20  35076  poimirlem24  35080  poimirlem28  35084  mblfinlem2  35094  mblfinlem4  35096  ismblfin  35097  el3v2  35652  atlatle  36615  pmaple  37056  dihglblem2N  38589  expgcd  39488  elnnrabdioph  39745  rabren3dioph  39753  zindbi  39884  expgrowth  41036  binomcxplemnotnn0  41057  trelpss  41156  etransc  42922  mogoldbb  44300  pgrple2abl  44764  aacllem  45326
  Copyright terms: Public domain W3C validator