Theorem mp3an12 1453

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 1450	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 690	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  mp3an12i  1467  ceqsalg  3472  brelrn  5884  predeq3  6253  funpr  6538  fvpr1  7128  fvpr2  7129  tfi  7786  peano5  7826  wrecseq3  8250  fpm  8802  0fsupp  9280  ssttrcl  9611  ac6  10374  alephadd  10471  axpre-sup  11063  cnegex2  11298  addlid  11299  renegcli  11425  div0OLD  11813  divclzi  11859  divcan1zi  11860  divcan2zi  11861  divreczi  11862  divcan3zi  11863  divcan4zi  11864  divasszi  11874  divmulzi  11875  divdirzi  11876  redivclzi  11890  ltm1  11966  mulgt1OLD  11983  recgt1i  12022  ltmul1i  12043  ltdiv1i  12044  ltmuldivi  12045  ltmul2i  12046  lemul1i  12047  lemul2i  12048  ledivp1i  12050  ltdivp1i  12051  nnge1  12156  nngt0  12159  nnrecgt0  12171  nnunb  12380  recnz  12551  eluzsubi  12768  ge0gtmnf  13074  x2times  13201  xrub  13214  xrge0neqmnf  13355  1mod  13807  m1expcl2  13992  1exp  13998  expubnd  14085  iexpcyc  14114  expnbnd  14139  expnlbnd  14140  faclbnd4lem1  14200  imval2  15058  cjdivi  15098  resqrex  15157  sqrtneglem  15173  absdivzi  15315  climcndslem1  15756  climcndslem2  15757  fprodge1  15902  bpoly3  15965  sinhval  16063  coshval  16064  ef01bndlem  16093  sin01gt0  16099  cos01gt0  16100  evend2  16268  divalglem5  16308  vdwlem13  16905  prmlem1  17019  prmlem2  17031  ress0  17154  frmdplusg  18728  m1expaddsub  19377  islindf4  21745  resstopn  23071  lecldbas  23104  hmphindis  23682  cnbl0  24659  xrsmopn  24699  zdis  24703  xrhmeo  24842  oprpiece1res1  24847  voliunlem3  25451  volsup  25455  volivth  25506  iblss2  25705  itgss  25711  coeidp  26167  dgrsub  26176  abelth  26349  reeff1olem  26354  sincosq1sgn  26405  sincosq3sgn  26407  sincosq4sgn  26408  sineq0  26431  logdivlt  26528  1cxp  26579  ecxp  26580  sinasin  26797  log2cnv  26852  efexple  27190  bposlem8  27200  lgsdir2lem2  27235  2sqb  27341  eqscut2  27718  scutun12  27722  eucliddivs  28272  pw2cut  28351  zs12bday  28365  axpaschlem  28889  axlowdimlem9  28899  axlowdimlem12  28902  axlowdimlem16  28906  axlowdimlem17  28907  sizusglecusg  29413  clwlkclwwlkf  29956  imsmetlem  30638  nmoubi  30720  nmobndi  30723  nmounbi  30724  nmlno0lem  30741  nmlnoubi  30744  isblo3i  30749  blometi  30751  blocni  30753  blocn2  30756  ipasslem2  30780  siii  30801  ubthlem1  30818  ubthlem2  30819  ubthlem3  30820  htthlem  30865  hvsubid  30974  hv2times  31009  hi01  31044  hhssabloilem  31209  pjsumi  31658  mayete3i  31676  hoaddcomi  31720  hodsi  31723  hoaddassi  31724  hocadddiri  31727  hocsubdiri  31728  hoaddridi  31734  honegsubi  31744  honegneg  31754  ho2times  31767  eigrei  31782  eigorthi  31785  nmopnegi  31913  hoddii  31937  lnophsi  31949  lnopeqi  31956  nmoptrii  32042  opsqrlem1  32088  opsqrlem6  32093  pjsdii  32103  pjddii  32104  pjscji  32118  pjssposi  32120  pjssdif2i  32122  pjtoi  32127  mdsl2bi  32271  cvmdi  32272  mdslmd3i  32280  mdslmd4i  32281  mdexchi  32283  cvati  32314  cvexchlem  32316  mdsymi  32359  dmdbr5ati  32370  cdj1i  32381  cdj3lem1  32382  xrge0infss  32712  xrge0tsmsd  33024  elrspunidl  33374  2sqr3nconstr  33764  cos9thpinconstrlem2  33773  rrhre  34004  esumpinfval  34056  oms0  34281  eulerpartlems  34344  eulerpartlemgf  34363  probmeasb  34414  acycgr2v  35143  cvmliftlem5  35282  bcneg1  35729  wsuceq3  35811  fullfunfv  35941  finminlem  36312  nn0prpwlem  36316  bj-ceqsalg0  36882  bj-ceqsalgALT  36884  bj-ceqsalgvALT  36886  bj-vtoclgfALT  37053  finxpreclem4  37388  sin2h  37610  cos2h  37611  tan2h  37612  poimirlem1  37621  poimirlem2  37622  poimirlem3  37623  poimirlem4  37624  poimirlem6  37626  poimirlem7  37627  poimirlem11  37631  poimirlem12  37632  poimirlem16  37636  poimirlem17  37637  poimirlem19  37639  poimirlem20  37640  poimirlem23  37643  poimirlem30  37650  poimirlem32  37652  poimir  37653  broucube  37654  mblfinlem1  37657  mblfinlem3  37659  mblfinlem4  37660  ismblfin  37661  volsupnfl  37665  iblmulc2nc  37685  ftc1anc  37701  dvasin  37704  heiborlem3  37813  heiborlem6  37816  heiborlem8  37818  cdleme32fva  40436  isnumbasgrplem1  43094  areaquad  43209  binomcxplemnotnn0  44349  permaxun  45005  fourierdlem101  46208  fourierdlem103  46210  fourierdlem104  46211  sqwvfourb  46230  fourierswlem  46231  fouriersw  46232  m1mod0mod1  47358  sgoldbeven3prm  47787  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  pgnbgreunbgrlem2lem3  48120  iooii  48922  aacllem  49806