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

Theorem mp3an12 1413
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 1410 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 706 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1037
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 1039
This theorem is referenced by:  mp3an12i  1427  ceqsalg  3228  ceqsralv  3232  brelrn  5354  predeq3  5682  funpr  5942  tfi  7050  peano5  7086  wrecseq3  7409  wfr3  7432  oneo  7658  nnneo  7728  fpm  7887  enerOLD  8000  unxpdomlem3  8163  0fsupp  8294  ackbij2  9062  ac6  9299  alephadd  9396  axgroth3  9650  axpre-sup  9987  mul02  10211  cnegex2  10215  addid2  10216  renegcli  10339  div0  10712  divclzi  10757  divcan1zi  10758  divcan2zi  10759  divreczi  10760  divcan3zi  10761  divcan4zi  10762  divasszi  10772  divmulzi  10773  divdirzi  10774  redivclzi  10788  ltm1  10860  mulgt1  10879  recgt1i  10917  recreclt  10919  ltmul1i  10939  ltdiv1i  10940  ltmuldivi  10941  ltmul2i  10942  lemul1i  10943  lemul2i  10944  ledivp1i  10946  ltdivp1i  10947  cju  11013  nnge1  11043  nngt0  11046  nnrecgt0  11055  nnunb  11285  elnnnn0c  11335  elnnz1  11400  recnz  11449  eluzsubi  11712  ge0gtmnf  12000  x2times  12126  xrub  12139  iccen  12314  1mod  12697  m1expcl2  12877  1exp  12884  expubnd  12916  iexpcyc  12964  expnbnd  12988  expnlbnd  12989  faclbnd4lem1  13075  remim  13851  imval2  13885  cjdivi  13925  resqrex  13985  sqrtneglem  14001  absdivzi  14140  iseraltlem2  14407  climcndslem1  14575  climcndslem2  14576  geo2lim  14600  bpoly3  14783  sinhval  14878  coshval  14879  ef01bndlem  14908  sin01gt0  14914  cos01gt0  14915  absefib  14922  efieq1re  14923  evend2  15075  divalglem5  15114  phiprmpw  15475  oddprm  15509  pythagtriplem1  15515  pythagtriplem11  15524  pythagtriplem13  15526  vdwlem13  15691  prmlem1  15808  prmlem2  15821  ress0  15928  frmdplusg  17385  symggen  17884  m1expaddsub  17912  psgnuni  17913  islindf4  20171  resstopn  20984  lecldbas  21017  hmphindis  21594  cnbl0  22571  xrsmopn  22609  zdis  22613  reperflem  22615  xrge0tsms  22631  xrhmeo  22739  oprpiece1res1  22744  cphsqrtcl  22978  ovolicopnf  23286  voliunlem3  23314  volsup  23318  volivth  23369  itg2seq  23503  itg2monolem2  23512  itgz  23541  ibl0  23547  iblss  23565  iblss2  23566  itgss  23572  itgeqa  23574  iblconst  23578  iblabsr  23590  iblmulc2  23591  itgsplit  23596  coeidp  24013  dgrsub  24022  aaliou3lem2  24092  abelth  24189  reeff1olem  24194  pilem3  24201  sincosq1sgn  24244  sincosq3sgn  24246  sincosq4sgn  24247  sineq0  24267  resinf1o  24276  efif1olem4  24285  logdivlti  24360  logdivlt  24361  efopn  24398  1cxp  24412  ecxp  24413  cxpsqrt  24443  isosctrlem1  24542  sinasin  24610  asinsin  24613  log2cnv  24665  basellem2  24802  basellem3  24803  isnsqf  24855  ppidif  24883  ppiublem1  24921  chtub  24931  efexple  25000  bposlem6  25008  bposlem8  25010  lgsdir2lem2  25045  2sqb  25151  ostth3  25321  axpaschlem  25814  axlowdimlem3  25818  axlowdimlem7  25822  axlowdimlem9  25824  axlowdimlem12  25827  axlowdimlem16  25831  axlowdimlem17  25832  axlowdim  25835  sizusglecusg  26353  imsmetlem  27529  nmoubi  27611  nmobndi  27614  nmounbi  27615  nmlno0lem  27632  nmlnoubi  27635  isblo3i  27640  blometi  27642  blocni  27644  blocn2  27647  ipasslem2  27671  siii  27692  ubthlem1  27710  ubthlem2  27711  ubthlem3  27712  htthlem  27758  hvsubid  27867  hv2times  27902  hi01  27937  hhssabloilem  28102  pjsumi  28553  mayete3i  28571  hoaddcomi  28615  hodsi  28618  hoaddassi  28619  hocadddiri  28622  hocsubdiri  28623  hoaddid1i  28629  honegsubi  28639  honegneg  28649  ho2times  28662  eigrei  28677  eigorthi  28680  nmopnegi  28808  hoddii  28832  lnophsi  28844  lnopeqi  28851  nmoptrii  28937  opsqrlem1  28983  opsqrlem6  28988  pjsdii  28998  pjddii  28999  pjscji  29013  pjssposi  29015  pjssdif2i  29017  pjtoi  29022  mdsl2bi  29166  cvmdi  29167  mdslmd3i  29175  mdslmd4i  29176  mdexchi  29178  cvati  29209  cvexchlem  29211  mdsymi  29254  dmdbr5ati  29265  cdj1i  29276  cdj3lem1  29277  xrge0infss  29510  xrge0tsmsd  29770  rrhre  30050  esumpinfval  30120  oms0  30344  eulerpartlems  30407  eulerpartlemgf  30426  probmeasb  30477  cvmliftlem5  31256  bcneg1  31608  wsuceq3  31747  scutun12  31901  fullfunfv  32038  finminlem  32296  nn0prpwlem  32301  bj-ceqsalg0  32861  bj-ceqsalgALT  32863  bj-ceqsalgvALT  32865  bj-vtoclgfALT  33005  finxpreclem4  33211  sin2h  33379  cos2h  33380  tan2h  33381  poimirlem1  33390  poimirlem2  33391  poimirlem3  33392  poimirlem4  33393  poimirlem6  33395  poimirlem7  33396  poimirlem11  33400  poimirlem12  33401  poimirlem16  33405  poimirlem17  33406  poimirlem19  33408  poimirlem20  33409  poimirlem23  33412  poimirlem30  33419  poimirlem32  33421  poimir  33422  broucube  33423  mblfinlem1  33426  mblfinlem3  33428  mblfinlem4  33429  ismblfin  33430  volsupnfl  33434  itg2addnclem3  33443  iblmulc2nc  33455  ftc1anc  33473  dvasin  33476  heiborlem3  33592  heiborlem6  33595  heiborlem8  33597  cdleme32fva  35551  isnumbasgrplem1  37497  areaquad  37628  binomcxplemnotnn0  38381  fourierdlem101  40193  fourierdlem103  40195  fourierdlem104  40196  sqwvfourb  40215  fourierswlem  40216  fouriersw  40217  m1mod0mod1  41109  sgoldbeven3prm  41442  aacllem  42318
  Copyright terms: Public domain W3C validator