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

Theorem mp3an12 1568
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 1565 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 673 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  mp3an12i  1582  ceqsalg  3424  ceqsralv  3428  brelrn  5557  predeq3  5897  funpr  6156  tfi  7283  peano5  7319  wrecseq3  7647  wfr3  7671  oneo  7898  nnneo  7968  fpm  8125  unxpdomlem3  8405  0fsupp  8536  ackbij2  9350  ac6  9587  alephadd  9684  axgroth3  9938  axpre-sup  10275  mul02  10499  cnegex2  10503  addid2  10504  renegcli  10627  div0  11000  divclzi  11045  divcan1zi  11046  divcan2zi  11047  divreczi  11048  divcan3zi  11049  divcan4zi  11050  divasszi  11060  divmulzi  11061  divdirzi  11062  redivclzi  11076  ltm1  11148  mulgt1  11167  recgt1i  11205  recreclt  11207  ltmul1i  11227  ltdiv1i  11228  ltmuldivi  11229  ltmul2i  11230  lemul1i  11231  lemul2i  11232  ledivp1i  11234  ltdivp1i  11235  cju  11301  nnge1  11332  nngt0  11335  nnrecgt0  11344  nnunb  11555  elnnnn0c  11604  elnnz1  11669  recnz  11718  eluzsubi  11932  ge0gtmnf  12221  x2times  12347  xrub  12360  iccen  12540  1mod  12926  m1expcl2  13105  1exp  13112  expubnd  13144  iexpcyc  13192  expnbnd  13216  expnlbnd  13217  faclbnd4lem1  13300  remim  14080  imval2  14114  cjdivi  14154  resqrex  14214  sqrtneglem  14230  absdivzi  14369  iseraltlem2  14636  climcndslem1  14803  climcndslem2  14804  geo2lim  14828  bpoly3  15009  sinhval  15104  coshval  15105  ef01bndlem  15134  sin01gt0  15140  cos01gt0  15141  absefib  15148  efieq1re  15149  evend2  15301  divalglem5  15340  phiprmpw  15698  pythagtriplem1  15738  pythagtriplem11  15747  pythagtriplem13  15749  vdwlem13  15914  prmlem1  16026  prmlem2  16038  ress0  16145  frmdplusg  17596  symggen  18091  m1expaddsub  18119  psgnuni  18120  islindf4  20387  resstopn  21204  lecldbas  21237  hmphindis  21814  cnbl0  22790  xrsmopn  22828  zdis  22832  reperflem  22834  xrge0tsms  22850  xrhmeo  22958  oprpiece1res1  22963  cphsqrtcl  23196  ovolicopnf  23505  voliunlem3  23533  volsup  23537  volivth  23588  itg2seq  23723  itg2monolem2  23732  itgz  23761  ibl0  23767  iblss  23785  iblss2  23786  itgss  23792  itgeqa  23794  iblconst  23798  iblabsr  23810  iblmulc2  23811  itgsplit  23816  coeidp  24233  dgrsub  24242  aaliou3lem2  24312  abelth  24409  reeff1olem  24414  pilem3OLD  24422  sincosq1sgn  24465  sincosq3sgn  24467  sincosq4sgn  24468  sineq0  24488  resinf1o  24497  efif1olem4  24506  logdivlti  24580  logdivlt  24581  efopn  24618  1cxp  24632  ecxp  24633  cxpsqrt  24663  isosctrlem1  24762  sinasin  24830  asinsin  24833  log2cnv  24885  basellem2  25022  basellem3  25023  isnsqf  25075  ppidif  25103  ppiublem1  25141  efexple  25220  bposlem6  25228  bposlem8  25230  lgsdir2lem2  25265  2sqb  25371  ostth3  25541  axpaschlem  26034  axlowdimlem3  26038  axlowdimlem7  26042  axlowdimlem9  26044  axlowdimlem12  26047  axlowdimlem16  26051  axlowdimlem17  26052  axlowdim  26055  sizusglecusg  26587  clwlkclwwlkf  27151  imsmetlem  27873  nmoubi  27955  nmobndi  27958  nmounbi  27959  nmlno0lem  27976  nmlnoubi  27979  isblo3i  27984  blometi  27986  blocni  27988  blocn2  27991  ipasslem2  28015  siii  28036  ubthlem1  28054  ubthlem2  28055  ubthlem3  28056  htthlem  28102  hvsubid  28211  hv2times  28246  hi01  28281  hhssabloilem  28446  pjsumi  28897  mayete3i  28915  hoaddcomi  28959  hodsi  28962  hoaddassi  28963  hocadddiri  28966  hocsubdiri  28967  hoaddid1i  28973  honegsubi  28983  honegneg  28993  ho2times  29006  eigrei  29021  eigorthi  29024  nmopnegi  29152  hoddii  29176  lnophsi  29188  lnopeqi  29195  nmoptrii  29281  opsqrlem1  29327  opsqrlem6  29332  pjsdii  29342  pjddii  29343  pjscji  29357  pjssposi  29359  pjssdif2i  29361  pjtoi  29366  mdsl2bi  29510  cvmdi  29511  mdslmd3i  29519  mdslmd4i  29520  mdexchi  29522  cvati  29553  cvexchlem  29555  mdsymi  29598  dmdbr5ati  29609  cdj1i  29620  cdj3lem1  29621  xrge0infss  29852  xrge0tsmsd  30110  rrhre  30390  esumpinfval  30460  oms0  30684  eulerpartlems  30747  eulerpartlemgf  30766  probmeasb  30817  cvmliftlem5  31594  bcneg1  31944  wsuceq3  32083  scutun12  32238  fullfunfv  32375  finminlem  32633  nn0prpwlem  32638  bj-ceqsalg0  33185  bj-ceqsalgALT  33187  bj-ceqsalgvALT  33189  bj-vtoclgfALT  33331  finxpreclem4  33547  sin2h  33712  cos2h  33713  tan2h  33714  poimirlem1  33723  poimirlem2  33724  poimirlem3  33725  poimirlem4  33726  poimirlem6  33728  poimirlem7  33729  poimirlem11  33733  poimirlem12  33734  poimirlem16  33738  poimirlem17  33739  poimirlem19  33741  poimirlem20  33742  poimirlem23  33745  poimirlem30  33752  poimirlem32  33754  poimir  33755  broucube  33756  mblfinlem1  33759  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  volsupnfl  33767  itg2addnclem3  33775  iblmulc2nc  33787  ftc1anc  33805  dvasin  33808  heiborlem3  33923  heiborlem6  33926  heiborlem8  33928  cdleme32fva  36218  isnumbasgrplem1  38172  areaquad  38302  binomcxplemnotnn0  39055  fourierdlem101  40903  fourierdlem103  40905  fourierdlem104  40906  sqwvfourb  40925  fourierswlem  40926  fouriersw  40927  m1mod0mod1  41914  sgoldbeven3prm  42246  aacllem  43118
  Copyright terms: Public domain W3C validator