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

Theorem mp3an12 1405
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 1402 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 701 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  mp3an12i  1419  ceqsalg  3199  ceqsralv  3203  brelrn  5261  predeq3  5584  funpr  5841  tfi  6919  peano5  6955  wrecseq3  7273  wfr3  7296  oneo  7522  nnneo  7592  fpm  7750  enerOLD  7863  unxpdomlem3  8025  0fsupp  8154  ackbij2  8922  ac6  9159  alephadd  9252  axgroth3  9506  axpre-sup  9843  mul02  10062  cnegex2  10066  addid2  10067  renegcli  10190  div0  10561  divclzi  10606  divcan1zi  10607  divcan2zi  10608  divreczi  10609  divcan3zi  10610  divcan4zi  10611  divasszi  10621  divmulzi  10622  divdirzi  10623  redivclzi  10637  ltm1  10709  mulgt1  10728  recgt1i  10766  recreclt  10768  ltmul1i  10788  ltdiv1i  10789  ltmuldivi  10790  ltmul2i  10791  lemul1i  10792  lemul2i  10793  ledivp1i  10795  ltdivp1i  10796  cju  10860  nnge1  10890  nngt0  10893  nnrecgt0  10902  nnunb  11132  elnnnn0c  11182  elnnz1  11233  recnz  11281  eluzsubi  11544  ge0gtmnf  11833  x2times  11955  xrub  11967  iccen  12141  1mod  12516  m1expcl2  12696  1exp  12703  expubnd  12735  iexpcyc  12783  expnbnd  12807  expnlbnd  12808  faclbnd4lem1  12894  remim  13648  imval2  13682  cjdivi  13722  resqrex  13782  sqrtneglem  13798  absdivzi  13937  iseraltlem2  14204  climcndslem1  14363  climcndslem2  14364  geo2lim  14388  bpoly3  14571  sinhval  14666  coshval  14667  ef01bndlem  14696  sin01gt0  14702  cos01gt0  14703  absefib  14710  efieq1re  14711  evend2  14862  divalglem5  14901  phiprmpw  15262  oddprm  15296  pythagtriplem1  15302  pythagtriplem11  15311  pythagtriplem13  15313  vdwlem13  15478  prmlem1  15595  prmlem2  15608  ress0  15704  frmdplusg  17157  symggen  17656  m1expaddsub  17684  psgnuni  17685  islindf4  19935  resstopn  20739  lecldbas  20772  hmphindis  21349  cnbl0  22316  xrsmopn  22352  zdis  22356  reperflem  22358  xrge0tsms  22374  xrhmeo  22481  oprpiece1res1  22486  cphsqrtcl  22713  ovolicopnf  23013  voliunlem3  23041  volsup  23045  volivth  23095  itg2seq  23229  itg2monolem2  23238  itgz  23267  ibl0  23273  iblss  23291  iblss2  23292  itgss  23298  itgeqa  23300  iblconst  23304  iblabsr  23316  iblmulc2  23317  itgsplit  23322  coeidp  23737  dgrsub  23746  aaliou3lem2  23816  abelth  23913  reeff1olem  23918  pilem3  23925  sincosq1sgn  23968  sincosq3sgn  23970  sincosq4sgn  23971  sineq0  23991  resinf1o  24000  efif1olem4  24009  logdivlti  24084  logdivlt  24085  efopn  24118  1cxp  24132  ecxp  24133  cxpsqrt  24163  isosctrlem1  24262  sinasin  24330  asinsin  24333  log2cnv  24385  basellem2  24522  basellem3  24523  isnsqf  24575  ppidif  24603  ppiublem1  24641  chtub  24651  efexple  24720  bposlem6  24728  bposlem8  24730  lgsdir2lem2  24765  2sqb  24871  ostth3  25041  axpaschlem  25535  axlowdimlem3  25539  axlowdimlem7  25543  axlowdimlem9  25545  axlowdimlem12  25548  axlowdimlem16  25552  axlowdimlem17  25553  axlowdim  25556  constr3trllem3  25943  imsmetlem  26723  nmoubi  26814  nmobndi  26817  nmounbi  26818  nmlno0lem  26835  nmlnoubi  26838  isblo3i  26843  blometi  26845  blocni  26847  blocn2  26850  ipasslem2  26874  siii  26895  ubthlem1  26913  ubthlem2  26914  ubthlem3  26915  htthlem  26961  hvsubid  27070  hv2times  27105  hi01  27140  hhssabloilem  27305  pjsumi  27756  mayete3i  27774  hoaddcomi  27818  hodsi  27821  hoaddassi  27822  hocadddiri  27825  hocsubdiri  27826  hoaddid1i  27832  honegsubi  27842  honegneg  27852  ho2times  27865  eigrei  27880  eigorthi  27883  nmopnegi  28011  hoddii  28035  lnophsi  28047  lnopeqi  28054  nmoptrii  28140  opsqrlem1  28186  opsqrlem6  28191  pjsdii  28201  pjddii  28202  pjscji  28216  pjssposi  28218  pjssdif2i  28220  pjtoi  28225  mdsl2bi  28369  cvmdi  28370  mdslmd3i  28378  mdslmd4i  28379  mdexchi  28381  cvati  28412  cvexchlem  28414  mdsymi  28457  dmdbr5ati  28468  cdj1i  28479  cdj3lem1  28480  xrge0infss  28718  xrge0tsmsd  28919  rrhre  29196  esumpinfval  29265  oms0  29489  eulerpartlems  29552  eulerpartlemgf  29571  probmeasb  29622  cvmliftlem5  30328  bcneg1  30678  wsuceq3  30810  fullfunfv  31027  finminlem  31285  nn0prpwlem  31290  bj-ceqsalg0  31871  bj-ceqsalgALT  31873  bj-ceqsalgvALT  31875  bj-vtoclgfALT  32012  finxpreclem4  32207  sin2h  32369  cos2h  32370  tan2h  32371  poimirlem1  32380  poimirlem2  32381  poimirlem3  32382  poimirlem4  32383  poimirlem6  32385  poimirlem7  32386  poimirlem11  32390  poimirlem12  32391  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  poimirlem23  32402  poimirlem30  32409  poimirlem32  32411  poimir  32412  broucube  32413  mblfinlem1  32416  mblfinlem3  32418  mblfinlem4  32419  ismblfin  32420  volsupnfl  32424  itg2addnclem3  32433  iblmulc2nc  32445  ftc1anc  32463  dvasin  32466  heiborlem3  32582  heiborlem6  32585  heiborlem8  32587  cdleme32fva  34543  isnumbasgrplem1  36490  areaquad  36621  binomcxplemnotnn0  37377  fourierdlem101  38901  fourierdlem103  38903  fourierdlem104  38904  sqwvfourb  38923  fourierswlem  38924  fouriersw  38925  m1mod0mod1  39751  sizusglecusg  40678  frgrwopreglem2  41481  aacllem  42316
  Copyright terms: Public domain W3C validator