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

Theorem mp3an12 1451
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 1448 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 688 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  mp3an12i  1465  ceqsalg  3477  ceqsralvOLD  3484  brelrn  5897  predeq3  6257  funpr  6557  fvpr1  7139  fvpr2  7141  tfi  7789  peano5  7830  peano5OLD  7831  wrecseq3  8251  wfr3OLD  8284  fpm  8813  0fsupp  9327  ssttrcl  9651  ac6  10416  alephadd  10513  axpre-sup  11105  cnegex2  11337  addid2  11338  renegcli  11462  div0  11843  divclzi  11890  divcan1zi  11891  divcan2zi  11892  divreczi  11893  divcan3zi  11894  divcan4zi  11895  divasszi  11905  divmulzi  11906  divdirzi  11907  redivclzi  11921  ltm1  11997  mulgt1  12014  recgt1i  12052  ltmul1i  12073  ltdiv1i  12074  ltmuldivi  12075  ltmul2i  12076  lemul1i  12077  lemul2i  12078  ledivp1i  12080  ltdivp1i  12081  nnge1  12181  nngt0  12184  nnrecgt0  12196  nnunb  12409  recnz  12578  eluzsubi  12796  ge0gtmnf  13091  x2times  13218  xrub  13231  xrge0neqmnf  13369  1mod  13808  m1expcl2  13991  1exp  13997  expubnd  14082  iexpcyc  14111  expnbnd  14135  expnlbnd  14136  faclbnd4lem1  14193  imval2  15036  cjdivi  15076  resqrex  15135  sqrtneglem  15151  absdivzi  15292  climcndslem1  15734  climcndslem2  15735  fprodge1  15878  bpoly3  15941  sinhval  16036  coshval  16037  ef01bndlem  16066  sin01gt0  16072  cos01gt0  16073  evend2  16239  divalglem5  16279  vdwlem13  16865  prmlem1  16980  prmlem2  16992  ress0  17124  frmdplusg  18664  m1expaddsub  19280  islindf4  21244  resstopn  22537  lecldbas  22570  hmphindis  23148  cnbl0  24137  xrsmopn  24175  zdis  24179  xrhmeo  24309  oprpiece1res1  24314  voliunlem3  24916  volsup  24920  volivth  24971  iblss2  25170  itgss  25176  coeidp  25624  dgrsub  25633  abelth  25800  reeff1olem  25805  sincosq1sgn  25855  sincosq3sgn  25857  sincosq4sgn  25858  sineq0  25880  logdivlt  25976  1cxp  26027  ecxp  26028  sinasin  26239  log2cnv  26294  efexple  26629  bposlem8  26639  lgsdir2lem2  26674  2sqb  26780  eqscut2  27145  scutun12  27149  axpaschlem  27889  axlowdimlem9  27899  axlowdimlem12  27902  axlowdimlem16  27906  axlowdimlem17  27907  sizusglecusg  28411  clwlkclwwlkf  28952  imsmetlem  29632  nmoubi  29714  nmobndi  29717  nmounbi  29718  nmlno0lem  29735  nmlnoubi  29738  isblo3i  29743  blometi  29745  blocni  29747  blocn2  29750  ipasslem2  29774  siii  29795  ubthlem1  29812  ubthlem2  29813  ubthlem3  29814  htthlem  29859  hvsubid  29968  hv2times  30003  hi01  30038  hhssabloilem  30203  pjsumi  30652  mayete3i  30670  hoaddcomi  30714  hodsi  30717  hoaddassi  30718  hocadddiri  30721  hocsubdiri  30722  hoaddid1i  30728  honegsubi  30738  honegneg  30748  ho2times  30761  eigrei  30776  eigorthi  30779  nmopnegi  30907  hoddii  30931  lnophsi  30943  lnopeqi  30950  nmoptrii  31036  opsqrlem1  31082  opsqrlem6  31087  pjsdii  31097  pjddii  31098  pjscji  31112  pjssposi  31114  pjssdif2i  31116  pjtoi  31121  mdsl2bi  31265  cvmdi  31266  mdslmd3i  31274  mdslmd4i  31275  mdexchi  31277  cvati  31308  cvexchlem  31310  mdsymi  31353  dmdbr5ati  31364  cdj1i  31375  cdj3lem1  31376  xrge0infss  31665  xrge0tsmsd  31899  elrspunidl  32203  rrhre  32602  esumpinfval  32672  oms0  32897  eulerpartlems  32960  eulerpartlemgf  32979  probmeasb  33030  acycgr2v  33744  cvmliftlem5  33883  bcneg1  34309  wsuceq3  34392  fullfunfv  34532  finminlem  34790  nn0prpwlem  34794  bj-ceqsalg0  35355  bj-ceqsalgALT  35357  bj-ceqsalgvALT  35359  bj-vtoclgfALT  35530  finxpreclem4  35865  sin2h  36068  cos2h  36069  tan2h  36070  poimirlem1  36079  poimirlem2  36080  poimirlem3  36081  poimirlem4  36082  poimirlem6  36084  poimirlem7  36085  poimirlem11  36089  poimirlem12  36090  poimirlem16  36094  poimirlem17  36095  poimirlem19  36097  poimirlem20  36098  poimirlem23  36101  poimirlem30  36108  poimirlem32  36110  poimir  36111  broucube  36112  mblfinlem1  36115  mblfinlem3  36117  mblfinlem4  36118  ismblfin  36119  volsupnfl  36123  iblmulc2nc  36143  ftc1anc  36159  dvasin  36162  heiborlem3  36272  heiborlem6  36275  heiborlem8  36277  cdleme32fva  38900  2xp3dxp2ge1d  40614  isnumbasgrplem1  41414  areaquad  41536  binomcxplemnotnn0  42626  fourierdlem101  44438  fourierdlem103  44440  fourierdlem104  44441  sqwvfourb  44460  fourierswlem  44461  fouriersw  44462  m1mod0mod1  45551  sgoldbeven3prm  45965  iooii  46940  aacllem  47238
  Copyright terms: Public domain W3C validator