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

Theorem mp3an12 1562
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 1559 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 670 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  mp3an12i  1576  ceqsalg  3382  ceqsralv  3386  brelrn  5494  predeq3  5827  funpr  6085  tfi  7200  peano5  7236  wrecseq3  7564  wfr3  7588  oneo  7815  nnneo  7885  fpm  8042  unxpdomlem3  8322  0fsupp  8453  ackbij2  9267  ac6  9504  alephadd  9601  axgroth3  9855  axpre-sup  10192  mul02  10416  cnegex2  10420  addid2  10421  renegcli  10544  div0  10917  divclzi  10962  divcan1zi  10963  divcan2zi  10964  divreczi  10965  divcan3zi  10966  divcan4zi  10967  divasszi  10977  divmulzi  10978  divdirzi  10979  redivclzi  10993  ltm1  11065  mulgt1  11084  recgt1i  11122  recreclt  11124  ltmul1i  11144  ltdiv1i  11145  ltmuldivi  11146  ltmul2i  11147  lemul1i  11148  lemul2i  11149  ledivp1i  11151  ltdivp1i  11152  cju  11218  nnge1  11248  nngt0  11251  nnrecgt0  11260  nnunb  11490  elnnnn0c  11540  elnnz1  11605  recnz  11654  eluzsubi  11916  ge0gtmnf  12208  x2times  12334  xrub  12347  iccen  12524  1mod  12910  m1expcl2  13089  1exp  13096  expubnd  13128  iexpcyc  13176  expnbnd  13200  expnlbnd  13201  faclbnd4lem1  13284  remim  14065  imval2  14099  cjdivi  14139  resqrex  14199  sqrtneglem  14215  absdivzi  14354  iseraltlem2  14621  climcndslem1  14788  climcndslem2  14789  geo2lim  14813  bpoly3  14995  sinhval  15090  coshval  15091  ef01bndlem  15120  sin01gt0  15126  cos01gt0  15127  absefib  15134  efieq1re  15135  evend2  15289  divalglem5  15328  phiprmpw  15688  pythagtriplem1  15728  pythagtriplem11  15737  pythagtriplem13  15739  vdwlem13  15904  prmlem1  16021  prmlem2  16034  ress0  16141  frmdplusg  17599  symggen  18097  m1expaddsub  18125  psgnuni  18126  islindf4  20394  resstopn  21211  lecldbas  21244  hmphindis  21821  cnbl0  22797  xrsmopn  22835  zdis  22839  reperflem  22841  xrge0tsms  22857  xrhmeo  22965  oprpiece1res1  22970  cphsqrtcl  23203  ovolicopnf  23512  voliunlem3  23540  volsup  23544  volivth  23595  itg2seq  23729  itg2monolem2  23738  itgz  23767  ibl0  23773  iblss  23791  iblss2  23792  itgss  23798  itgeqa  23800  iblconst  23804  iblabsr  23816  iblmulc2  23817  itgsplit  23822  coeidp  24239  dgrsub  24248  aaliou3lem2  24318  abelth  24415  reeff1olem  24420  pilem3OLD  24428  sincosq1sgn  24471  sincosq3sgn  24473  sincosq4sgn  24474  sineq0  24494  resinf1o  24503  efif1olem4  24512  logdivlti  24587  logdivlt  24588  efopn  24625  1cxp  24639  ecxp  24640  cxpsqrt  24670  isosctrlem1  24769  sinasin  24837  asinsin  24840  log2cnv  24892  basellem2  25029  basellem3  25030  isnsqf  25082  ppidif  25110  ppiublem1  25148  efexple  25227  bposlem6  25235  bposlem8  25237  lgsdir2lem2  25272  2sqb  25378  ostth3  25548  axpaschlem  26041  axlowdimlem3  26045  axlowdimlem7  26049  axlowdimlem9  26051  axlowdimlem12  26054  axlowdimlem16  26058  axlowdimlem17  26059  axlowdim  26062  sizusglecusg  26594  clwlkclwwlkf  27158  imsmetlem  27885  nmoubi  27967  nmobndi  27970  nmounbi  27971  nmlno0lem  27988  nmlnoubi  27991  isblo3i  27996  blometi  27998  blocni  28000  blocn2  28003  ipasslem2  28027  siii  28048  ubthlem1  28066  ubthlem2  28067  ubthlem3  28068  htthlem  28114  hvsubid  28223  hv2times  28258  hi01  28293  hhssabloilem  28458  pjsumi  28909  mayete3i  28927  hoaddcomi  28971  hodsi  28974  hoaddassi  28975  hocadddiri  28978  hocsubdiri  28979  hoaddid1i  28985  honegsubi  28995  honegneg  29005  ho2times  29018  eigrei  29033  eigorthi  29036  nmopnegi  29164  hoddii  29188  lnophsi  29200  lnopeqi  29207  nmoptrii  29293  opsqrlem1  29339  opsqrlem6  29344  pjsdii  29354  pjddii  29355  pjscji  29369  pjssposi  29371  pjssdif2i  29373  pjtoi  29378  mdsl2bi  29522  cvmdi  29523  mdslmd3i  29531  mdslmd4i  29532  mdexchi  29534  cvati  29565  cvexchlem  29567  mdsymi  29610  dmdbr5ati  29621  cdj1i  29632  cdj3lem1  29633  xrge0infss  29865  xrge0tsmsd  30125  rrhre  30405  esumpinfval  30475  oms0  30699  eulerpartlems  30762  eulerpartlemgf  30781  probmeasb  30832  cvmliftlem5  31609  bcneg1  31960  wsuceq3  32099  scutun12  32254  fullfunfv  32391  finminlem  32649  nn0prpwlem  32654  bj-ceqsalg0  33206  bj-ceqsalgALT  33208  bj-ceqsalgvALT  33210  bj-vtoclgfALT  33352  finxpreclem4  33568  sin2h  33732  cos2h  33733  tan2h  33734  poimirlem1  33743  poimirlem2  33744  poimirlem3  33745  poimirlem4  33746  poimirlem6  33748  poimirlem7  33749  poimirlem11  33753  poimirlem12  33754  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem23  33765  poimirlem30  33772  poimirlem32  33774  poimir  33775  broucube  33776  mblfinlem1  33779  mblfinlem3  33781  mblfinlem4  33782  ismblfin  33783  volsupnfl  33787  itg2addnclem3  33795  iblmulc2nc  33807  ftc1anc  33825  dvasin  33828  heiborlem3  33944  heiborlem6  33947  heiborlem8  33949  cdleme32fva  36246  isnumbasgrplem1  38197  areaquad  38328  binomcxplemnotnn0  39081  fourierdlem101  40941  fourierdlem103  40943  fourierdlem104  40944  sqwvfourb  40963  fourierswlem  40964  fouriersw  40965  m1mod0mod1  41867  sgoldbeven3prm  42199  aacllem  43078
  Copyright terms: Public domain W3C validator