Theorem mp3an12 1406

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  mp3an12i  1420  ceqsalg  3203  ceqsralv  3207  brelrn  5277  predeq3  5601  funpr  5858  tfi  6945  peano5  6981  wrecseq3  7299  wfr3  7322  oneo  7548  nnneo  7618  fpm  7776  enerOLD  7889  unxpdomlem3  8051  0fsupp  8180  ackbij2  8948  ac6  9185  alephadd  9278  axgroth3  9532  axpre-sup  9869  mul02  10093  cnegex2  10097  addid2  10098  renegcli  10221  div0  10594  divclzi  10639  divcan1zi  10640  divcan2zi  10641  divreczi  10642  divcan3zi  10643  divcan4zi  10644  divasszi  10654  divmulzi  10655  divdirzi  10656  redivclzi  10670  ltm1  10742  mulgt1  10761  recgt1i  10799  recreclt  10801  ltmul1i  10821  ltdiv1i  10822  ltmuldivi  10823  ltmul2i  10824  lemul1i  10825  lemul2i  10826  ledivp1i  10828  ltdivp1i  10829  cju  10893  nnge1  10923  nngt0  10926  nnrecgt0  10935  nnunb  11165  elnnnn0c  11215  elnnz1  11280  recnz  11328  eluzsubi  11591  ge0gtmnf  11877  x2times  12001  xrub  12014  iccen  12188  1mod  12564  m1expcl2  12744  1exp  12751  expubnd  12783  iexpcyc  12831  expnbnd  12855  expnlbnd  12856  faclbnd4lem1  12942  remim  13705  imval2  13739  cjdivi  13779  resqrex  13839  sqrtneglem  13855  absdivzi  13994  iseraltlem2  14261  climcndslem1  14420  climcndslem2  14421  geo2lim  14445  bpoly3  14628  sinhval  14723  coshval  14724  ef01bndlem  14753  sin01gt0  14759  cos01gt0  14760  absefib  14767  efieq1re  14768  evend2  14919  divalglem5  14958  phiprmpw  15319  oddprm  15353  pythagtriplem1  15359  pythagtriplem11  15368  pythagtriplem13  15370  vdwlem13  15535  prmlem1  15652  prmlem2  15665  ress0  15761  frmdplusg  17214  symggen  17713  m1expaddsub  17741  psgnuni  17742  islindf4  19996  resstopn  20800  lecldbas  20833  hmphindis  21410  cnbl0  22387  xrsmopn  22423  zdis  22427  reperflem  22429  xrge0tsms  22445  xrhmeo  22553  oprpiece1res1  22558  cphsqrtcl  22792  ovolicopnf  23099  voliunlem3  23127  volsup  23131  volivth  23181  itg2seq  23315  itg2monolem2  23324  itgz  23353  ibl0  23359  iblss  23377  iblss2  23378  itgss  23384  itgeqa  23386  iblconst  23390  iblabsr  23402  iblmulc2  23403  itgsplit  23408  coeidp  23823  dgrsub  23832  aaliou3lem2  23902  abelth  23999  reeff1olem  24004  pilem3  24011  sincosq1sgn  24054  sincosq3sgn  24056  sincosq4sgn  24057  sineq0  24077  resinf1o  24086  efif1olem4  24095  logdivlti  24170  logdivlt  24171  efopn  24204  1cxp  24218  ecxp  24219  cxpsqrt  24249  isosctrlem1  24348  sinasin  24416  asinsin  24419  log2cnv  24471  basellem2  24608  basellem3  24609  isnsqf  24661  ppidif  24689  ppiublem1  24727  chtub  24737  efexple  24806  bposlem6  24814  bposlem8  24816  lgsdir2lem2  24851  2sqb  24957  ostth3  25127  axpaschlem  25620  axlowdimlem3  25624  axlowdimlem7  25628  axlowdimlem9  25630  axlowdimlem12  25633  axlowdimlem16  25637  axlowdimlem17  25638  axlowdim  25641  constr3trllem3  26180  imsmetlem  26929  nmoubi  27011  nmobndi  27014  nmounbi  27015  nmlno0lem  27032  nmlnoubi  27035  isblo3i  27040  blometi  27042  blocni  27044  blocn2  27047  ipasslem2  27071  siii  27092  ubthlem1  27110  ubthlem2  27111  ubthlem3  27112  htthlem  27158  hvsubid  27267  hv2times  27302  hi01  27337  hhssabloilem  27502  pjsumi  27953  mayete3i  27971  hoaddcomi  28015  hodsi  28018  hoaddassi  28019  hocadddiri  28022  hocsubdiri  28023  hoaddid1i  28029  honegsubi  28039  honegneg  28049  ho2times  28062  eigrei  28077  eigorthi  28080  nmopnegi  28208  hoddii  28232  lnophsi  28244  lnopeqi  28251  nmoptrii  28337  opsqrlem1  28383  opsqrlem6  28388  pjsdii  28398  pjddii  28399  pjscji  28413  pjssposi  28415  pjssdif2i  28417  pjtoi  28422  mdsl2bi  28566  cvmdi  28567  mdslmd3i  28575  mdslmd4i  28576  mdexchi  28578  cvati  28609  cvexchlem  28611  mdsymi  28654  dmdbr5ati  28665  cdj1i  28676  cdj3lem1  28677  xrge0infss  28915  xrge0tsmsd  29116  rrhre  29393  esumpinfval  29462  oms0  29686  eulerpartlems  29749  eulerpartlemgf  29768  probmeasb  29819  cvmliftlem5  30525  bcneg1  30875  wsuceq3  31007  fullfunfv  31224  finminlem  31482  nn0prpwlem  31487  bj-ceqsalg0  32071  bj-ceqsalgALT  32073  bj-ceqsalgvALT  32075  bj-vtoclgfALT  32212  finxpreclem4  32407  sin2h  32569  cos2h  32570  tan2h  32571  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  poimirlem30  32609  poimirlem32  32611  poimir  32612  broucube  32613  mblfinlem1  32616  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  volsupnfl  32624  itg2addnclem3  32633  iblmulc2nc  32645  ftc1anc  32663  dvasin  32666  heiborlem3  32782  heiborlem6  32785  heiborlem8  32787  cdleme32fva  34743  isnumbasgrplem1  36690  areaquad  36821  binomcxplemnotnn0  37577  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  m1mod0mod1  39949  sizusglecusg  40679  frgrwopreglem2  41482  aacllem  42356