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

Theorem mp3an12 1442
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 1439 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 686 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  mp3an12i  1456  ceqsalg  3530  ceqsralv  3534  brelrn  5806  predeq3  6146  funpr  6404  tfi  7556  peano5  7593  wrecseq3  7943  wfr3  7966  fpm  8429  0fsupp  8844  ac6  9891  alephadd  9988  axpre-sup  10580  cnegex2  10811  addid2  10812  renegcli  10936  div0  11317  divclzi  11364  divcan1zi  11365  divcan2zi  11366  divreczi  11367  divcan3zi  11368  divcan4zi  11369  divasszi  11379  divmulzi  11380  divdirzi  11381  redivclzi  11395  ltm1  11471  mulgt1  11488  recgt1i  11526  ltmul1i  11547  ltdiv1i  11548  ltmuldivi  11549  ltmul2i  11550  lemul1i  11551  lemul2i  11552  ledivp1i  11554  ltdivp1i  11555  nnge1  11654  nngt0  11657  nnrecgt0  11669  nnunb  11882  recnz  12046  ge0gtmnf  12555  x2times  12682  xrub  12695  xrge0neqmnf  12830  1mod  13261  m1expcl2  13441  1exp  13448  expubnd  13531  iexpcyc  13559  expnbnd  13583  expnlbnd  13584  faclbnd4lem1  13643  imval2  14500  cjdivi  14540  resqrex  14600  sqrtneglem  14616  absdivzi  14757  climcndslem1  15194  climcndslem2  15195  fprodge1  15339  bpoly3  15402  sinhval  15497  coshval  15498  ef01bndlem  15527  sin01gt0  15533  cos01gt0  15534  evend2  15696  divalglem5  15738  vdwlem13  16319  prmlem1  16431  prmlem2  16443  ress0  16548  frmdplusg  18009  m1expaddsub  18557  islindf4  20912  resstopn  21724  lecldbas  21757  hmphindis  22335  cnbl0  23311  xrsmopn  23349  zdis  23353  xrhmeo  23479  oprpiece1res1  23484  voliunlem3  24082  volsup  24086  volivth  24137  iblss2  24335  itgss  24341  coeidp  24782  dgrsub  24791  abelth  24958  reeff1olem  24963  sincosq1sgn  25013  sincosq3sgn  25015  sincosq4sgn  25016  sineq0  25038  logdivlt  25131  1cxp  25182  ecxp  25183  sinasin  25394  log2cnv  25450  efexple  25785  bposlem8  25795  lgsdir2lem2  25830  2sqb  25936  axpaschlem  26654  axlowdimlem9  26664  axlowdimlem12  26667  axlowdimlem16  26671  axlowdimlem17  26672  sizusglecusg  27173  clwlkclwwlkf  27714  imsmetlem  28395  nmoubi  28477  nmobndi  28480  nmounbi  28481  nmlno0lem  28498  nmlnoubi  28501  isblo3i  28506  blometi  28508  blocni  28510  blocn2  28513  ipasslem2  28537  siii  28558  ubthlem1  28575  ubthlem2  28576  ubthlem3  28577  htthlem  28622  hvsubid  28731  hv2times  28766  hi01  28801  hhssabloilem  28966  pjsumi  29415  mayete3i  29433  hoaddcomi  29477  hodsi  29480  hoaddassi  29481  hocadddiri  29484  hocsubdiri  29485  hoaddid1i  29491  honegsubi  29501  honegneg  29511  ho2times  29524  eigrei  29539  eigorthi  29542  nmopnegi  29670  hoddii  29694  lnophsi  29706  lnopeqi  29713  nmoptrii  29799  opsqrlem1  29845  opsqrlem6  29850  pjsdii  29860  pjddii  29861  pjscji  29875  pjssposi  29877  pjssdif2i  29879  pjtoi  29884  mdsl2bi  30028  cvmdi  30029  mdslmd3i  30037  mdslmd4i  30038  mdexchi  30040  cvati  30071  cvexchlem  30073  mdsymi  30116  dmdbr5ati  30127  cdj1i  30138  cdj3lem1  30139  xrge0infss  30411  xrge0tsmsd  30620  rrhre  31162  esumpinfval  31232  oms0  31455  eulerpartlems  31518  eulerpartlemgf  31537  probmeasb  31588  acycgr2v  32295  cvmliftlem5  32434  bcneg1  32866  wsuceq3  33002  scutun12  33169  fullfunfv  33306  finminlem  33564  nn0prpwlem  33568  bj-ceqsalg0  34102  bj-ceqsalgALT  34104  bj-ceqsalgvALT  34106  bj-vtoclgfALT  34247  finxpreclem4  34558  sin2h  34764  cos2h  34765  tan2h  34766  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem4  34778  poimirlem6  34780  poimirlem7  34781  poimirlem11  34785  poimirlem12  34786  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem23  34797  poimirlem30  34804  poimirlem32  34806  poimir  34807  broucube  34808  mblfinlem1  34811  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  volsupnfl  34819  itg2addnclem3  34827  iblmulc2nc  34839  ftc1anc  34857  dvasin  34860  heiborlem3  34974  heiborlem6  34977  heiborlem8  34979  cdleme32fva  37455  isnumbasgrplem1  39581  areaquad  39703  binomcxplemnotnn0  40568  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  m1mod0mod1  43410  sgoldbeven3prm  43795  aacllem  44800
  Copyright terms: Public domain W3C validator