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

Theorem mp3an12 1412
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mp3an12.1 𝜑
mp3an12.2 𝜓
mp3an12.3 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an12 (𝜒𝜃)

Proof of Theorem mp3an12
StepHypRef Expression
1 mp3an12.2 . 2 𝜓
2 mp3an12.1 . . 3 𝜑
3 mp3an12.3 . . 3 ((𝜑𝜓𝜒) → 𝜃)
42, 3mp3an1 1409 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 705 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  mp3an12i  1426  ceqsalg  3225  ceqsralv  3229  brelrn  5345  predeq3  5672  funpr  5932  tfi  7038  peano5  7074  wrecseq3  7397  wfr3  7420  oneo  7646  nnneo  7716  fpm  7875  enerOLD  7988  unxpdomlem3  8151  0fsupp  8282  ackbij2  9050  ac6  9287  alephadd  9384  axgroth3  9638  axpre-sup  9975  mul02  10199  cnegex2  10203  addid2  10204  renegcli  10327  div0  10700  divclzi  10745  divcan1zi  10746  divcan2zi  10747  divreczi  10748  divcan3zi  10749  divcan4zi  10750  divasszi  10760  divmulzi  10761  divdirzi  10762  redivclzi  10776  ltm1  10848  mulgt1  10867  recgt1i  10905  recreclt  10907  ltmul1i  10927  ltdiv1i  10928  ltmuldivi  10929  ltmul2i  10930  lemul1i  10931  lemul2i  10932  ledivp1i  10934  ltdivp1i  10935  cju  11001  nnge1  11031  nngt0  11034  nnrecgt0  11043  nnunb  11273  elnnnn0c  11323  elnnz1  11388  recnz  11437  eluzsubi  11700  ge0gtmnf  11988  x2times  12114  xrub  12127  iccen  12302  1mod  12685  m1expcl2  12865  1exp  12872  expubnd  12904  iexpcyc  12952  expnbnd  12976  expnlbnd  12977  faclbnd4lem1  13063  remim  13838  imval2  13872  cjdivi  13912  resqrex  13972  sqrtneglem  13988  absdivzi  14127  iseraltlem2  14394  climcndslem1  14562  climcndslem2  14563  geo2lim  14587  bpoly3  14770  sinhval  14865  coshval  14866  ef01bndlem  14895  sin01gt0  14901  cos01gt0  14902  absefib  14909  efieq1re  14910  evend2  15062  divalglem5  15101  phiprmpw  15462  oddprm  15496  pythagtriplem1  15502  pythagtriplem11  15511  pythagtriplem13  15513  vdwlem13  15678  prmlem1  15795  prmlem2  15808  ress0  15915  frmdplusg  17372  symggen  17871  m1expaddsub  17899  psgnuni  17900  islindf4  20158  resstopn  20971  lecldbas  21004  hmphindis  21581  cnbl0  22558  xrsmopn  22596  zdis  22600  reperflem  22602  xrge0tsms  22618  xrhmeo  22726  oprpiece1res1  22731  cphsqrtcl  22965  ovolicopnf  23273  voliunlem3  23301  volsup  23305  volivth  23356  itg2seq  23490  itg2monolem2  23499  itgz  23528  ibl0  23534  iblss  23552  iblss2  23553  itgss  23559  itgeqa  23561  iblconst  23565  iblabsr  23577  iblmulc2  23578  itgsplit  23583  coeidp  24000  dgrsub  24009  aaliou3lem2  24079  abelth  24176  reeff1olem  24181  pilem3  24188  sincosq1sgn  24231  sincosq3sgn  24233  sincosq4sgn  24234  sineq0  24254  resinf1o  24263  efif1olem4  24272  logdivlti  24347  logdivlt  24348  efopn  24385  1cxp  24399  ecxp  24400  cxpsqrt  24430  isosctrlem1  24529  sinasin  24597  asinsin  24600  log2cnv  24652  basellem2  24789  basellem3  24790  isnsqf  24842  ppidif  24870  ppiublem1  24908  chtub  24918  efexple  24987  bposlem6  24995  bposlem8  24997  lgsdir2lem2  25032  2sqb  25138  ostth3  25308  axpaschlem  25801  axlowdimlem3  25805  axlowdimlem7  25809  axlowdimlem9  25811  axlowdimlem12  25814  axlowdimlem16  25818  axlowdimlem17  25819  axlowdim  25822  sizusglecusg  26340  imsmetlem  27515  nmoubi  27597  nmobndi  27600  nmounbi  27601  nmlno0lem  27618  nmlnoubi  27621  isblo3i  27626  blometi  27628  blocni  27630  blocn2  27633  ipasslem2  27657  siii  27678  ubthlem1  27696  ubthlem2  27697  ubthlem3  27698  htthlem  27744  hvsubid  27853  hv2times  27888  hi01  27923  hhssabloilem  28088  pjsumi  28539  mayete3i  28557  hoaddcomi  28601  hodsi  28604  hoaddassi  28605  hocadddiri  28608  hocsubdiri  28609  hoaddid1i  28615  honegsubi  28625  honegneg  28635  ho2times  28648  eigrei  28663  eigorthi  28666  nmopnegi  28794  hoddii  28818  lnophsi  28830  lnopeqi  28837  nmoptrii  28923  opsqrlem1  28969  opsqrlem6  28974  pjsdii  28984  pjddii  28985  pjscji  28999  pjssposi  29001  pjssdif2i  29003  pjtoi  29008  mdsl2bi  29152  cvmdi  29153  mdslmd3i  29161  mdslmd4i  29162  mdexchi  29164  cvati  29195  cvexchlem  29197  mdsymi  29240  dmdbr5ati  29251  cdj1i  29262  cdj3lem1  29263  xrge0infss  29499  xrge0tsmsd  29759  rrhre  30039  esumpinfval  30109  oms0  30333  eulerpartlems  30396  eulerpartlemgf  30415  probmeasb  30466  cvmliftlem5  31245  bcneg1  31597  wsuceq3  31737  scutun12  31891  fullfunfv  32029  finminlem  32287  nn0prpwlem  32292  bj-ceqsalg0  32852  bj-ceqsalgALT  32854  bj-ceqsalgvALT  32856  bj-vtoclgfALT  32996  finxpreclem4  33202  sin2h  33370  cos2h  33371  tan2h  33372  poimirlem1  33381  poimirlem2  33382  poimirlem3  33383  poimirlem4  33384  poimirlem6  33386  poimirlem7  33387  poimirlem11  33391  poimirlem12  33392  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem23  33403  poimirlem30  33410  poimirlem32  33412  poimir  33413  broucube  33414  mblfinlem1  33417  mblfinlem3  33419  mblfinlem4  33420  ismblfin  33421  volsupnfl  33425  itg2addnclem3  33434  iblmulc2nc  33446  ftc1anc  33464  dvasin  33467  heiborlem3  33583  heiborlem6  33586  heiborlem8  33588  cdleme32fva  35544  isnumbasgrplem1  37490  areaquad  37621  binomcxplemnotnn0  38375  fourierdlem101  40187  fourierdlem103  40189  fourierdlem104  40190  sqwvfourb  40209  fourierswlem  40210  fouriersw  40211  m1mod0mod1  41103  sgoldbeven3prm  41436  aacllem  42312
  Copyright terms: Public domain W3C validator