Theorem mp3an12 1454

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

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 ⊢ 𝜓
2		mp3an12.1	. . 3 ⊢ 𝜑
3		mp3an12.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an1 1451	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 691	1 ⊢ (𝜒 → 𝜃)

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  mp3an12i  1468  ceqsalg  3466  brelrn  5898  predeq3  6270  funpr  6555  fvpr1  7147  fvpr2  7148  tfi  7804  peano5  7844  wrecseq3  8267  fpm  8823  0fsupp  9303  ssttrcl  9636  ac6  10402  alephadd  10500  axpre-sup  11092  cnegex2  11328  addlid  11329  renegcli  11455  div0OLD  11843  divclzi  11890  divcan1zi  11891  divcan2zi  11892  divreczi  11893  divcan3zi  11894  divcan4zi  11895  divasszi  11905  divmulzi  11906  divdirzi  11907  redivclzi  11921  ltm1  11997  mulgt1OLD  12014  recgt1i  12053  ltmul1i  12074  ltdiv1i  12075  ltmuldivi  12076  ltmul2i  12077  lemul1i  12078  lemul2i  12079  ledivp1i  12081  ltdivp1i  12082  nnge1  12205  nngt0  12208  nnrecgt0  12220  nnunb  12433  recnz  12604  eluzsubi  12820  ge0gtmnf  13124  x2times  13251  xrub  13264  xrge0neqmnf  13405  1mod  13862  m1expcl2  14047  1exp  14053  expubnd  14140  iexpcyc  14169  expnbnd  14194  expnlbnd  14195  faclbnd4lem1  14255  imval2  15113  cjdivi  15153  resqrex  15212  sqrtneglem  15228  absdivzi  15370  climcndslem1  15814  climcndslem2  15815  fprodge1  15960  bpoly3  16023  sinhval  16121  coshval  16122  ef01bndlem  16151  sin01gt0  16157  cos01gt0  16158  evend2  16326  divalglem5  16366  vdwlem13  16964  prmlem1  17078  prmlem2  17090  ress0  17213  frmdplusg  18822  m1expaddsub  19473  islindf4  21818  resstopn  23151  lecldbas  23184  hmphindis  23762  cnbl0  24738  xrsmopn  24778  zdis  24782  xrhmeo  24913  oprpiece1res1  24918  voliunlem3  25519  volsup  25523  volivth  25574  iblss2  25773  itgss  25779  coeidp  26228  dgrsub  26237  abelth  26406  reeff1olem  26411  sincosq1sgn  26462  sincosq3sgn  26464  sincosq4sgn  26465  sineq0  26488  logdivlt  26585  1cxp  26636  ecxp  26637  sinasin  26853  log2cnv  26908  efexple  27244  bposlem8  27254  lgsdir2lem2  27289  2sqb  27395  eqcuts2  27778  cutsun12  27782  eucliddivs  28368  pw2cut  28452  axpaschlem  29009  axlowdimlem9  29019  axlowdimlem12  29022  axlowdimlem16  29026  axlowdimlem17  29027  sizusglecusg  29532  clwlkclwwlkf  30078  imsmetlem  30761  nmoubi  30843  nmobndi  30846  nmounbi  30847  nmlno0lem  30864  nmlnoubi  30867  isblo3i  30872  blometi  30874  blocni  30876  blocn2  30879  ipasslem2  30903  siii  30924  ubthlem1  30941  ubthlem2  30942  ubthlem3  30943  htthlem  30988  hvsubid  31097  hv2times  31132  hi01  31167  hhssabloilem  31332  pjsumi  31781  mayete3i  31799  hoaddcomi  31843  hodsi  31846  hoaddassi  31847  hocadddiri  31850  hocsubdiri  31851  hoaddridi  31857  honegsubi  31867  honegneg  31877  ho2times  31890  eigrei  31905  eigorthi  31908  nmopnegi  32036  hoddii  32060  lnophsi  32072  lnopeqi  32079  nmoptrii  32165  opsqrlem1  32211  opsqrlem6  32216  pjsdii  32226  pjddii  32227  pjscji  32241  pjssposi  32243  pjssdif2i  32245  pjtoi  32250  mdsl2bi  32394  cvmdi  32395  mdslmd3i  32403  mdslmd4i  32404  mdexchi  32406  cvati  32437  cvexchlem  32439  mdsymi  32482  dmdbr5ati  32493  cdj1i  32504  cdj3lem1  32505  xrge0infss  32833  xrge0tsmsd  33134  elrspunidl  33488  2sqr3nconstr  33925  cos9thpinconstrlem2  33934  rrhre  34165  esumpinfval  34217  oms0  34441  eulerpartlems  34504  eulerpartlemgf  34523  probmeasb  34574  acycgr2v  35332  cvmliftlem5  35471  bcneg1  35918  wsuceq3  35997  fullfunfv  36129  finminlem  36500  nn0prpwlem  36504  regsfromunir1  36722  bj-ceqsalg0  37195  bj-ceqsalgALT  37197  bj-ceqsalgvALT  37199  bj-vtoclgfALT  37366  finxpreclem4  37710  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem30  37971  poimirlem32  37973  poimir  37974  broucube  37975  mblfinlem1  37978  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  volsupnfl  37986  iblmulc2nc  38006  ftc1anc  38022  dvasin  38025  heiborlem3  38134  heiborlem6  38137  heiborlem8  38139  cdleme32fva  40883  isnumbasgrplem1  43529  areaquad  43644  binomcxplemnotnn0  44783  permaxun  45438  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  m1mod0mod1  47802  sgoldbeven3prm  48253  pgnbgreunbgrlem2lem1  48584  pgnbgreunbgrlem2lem2  48585  pgnbgreunbgrlem2lem3  48586  iooii  49387  aacllem  50270