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  3475  brelrn  5890  predeq3  6262  funpr  6547  fvpr1  7138  fvpr2  7139  tfi  7795  peano5  7835  wrecseq3  8259  fpm  8815  0fsupp  9295  ssttrcl  9626  ac6  10392  alephadd  10490  axpre-sup  11082  cnegex2  11317  addlid  11318  renegcli  11444  div0OLD  11832  divclzi  11878  divcan1zi  11879  divcan2zi  11880  divreczi  11881  divcan3zi  11882  divcan4zi  11883  divasszi  11893  divmulzi  11894  divdirzi  11895  redivclzi  11909  ltm1  11985  mulgt1OLD  12002  recgt1i  12041  ltmul1i  12062  ltdiv1i  12063  ltmuldivi  12064  ltmul2i  12065  lemul1i  12066  lemul2i  12067  ledivp1i  12069  ltdivp1i  12070  nnge1  12175  nngt0  12178  nnrecgt0  12190  nnunb  12399  recnz  12569  eluzsubi  12785  ge0gtmnf  13089  x2times  13216  xrub  13229  xrge0neqmnf  13370  1mod  13825  m1expcl2  14010  1exp  14016  expubnd  14103  iexpcyc  14132  expnbnd  14157  expnlbnd  14158  faclbnd4lem1  14218  imval2  15076  cjdivi  15116  resqrex  15175  sqrtneglem  15191  absdivzi  15333  climcndslem1  15774  climcndslem2  15775  fprodge1  15920  bpoly3  15983  sinhval  16081  coshval  16082  ef01bndlem  16111  sin01gt0  16117  cos01gt0  16118  evend2  16286  divalglem5  16326  vdwlem13  16923  prmlem1  17037  prmlem2  17049  ress0  17172  frmdplusg  18781  m1expaddsub  19429  islindf4  21795  resstopn  23132  lecldbas  23165  hmphindis  23743  cnbl0  24719  xrsmopn  24759  zdis  24763  xrhmeo  24902  oprpiece1res1  24907  voliunlem3  25511  volsup  25515  volivth  25566  iblss2  25765  itgss  25771  coeidp  26227  dgrsub  26236  abelth  26409  reeff1olem  26414  sincosq1sgn  26465  sincosq3sgn  26467  sincosq4sgn  26468  sineq0  26491  logdivlt  26588  1cxp  26639  ecxp  26640  sinasin  26857  log2cnv  26912  efexple  27250  bposlem8  27260  lgsdir2lem2  27295  2sqb  27401  eqscut2  27782  scutun12  27786  eucliddivs  28353  pw2cut  28437  bdayfinbndlem1  28444  axpaschlem  28994  axlowdimlem9  29004  axlowdimlem12  29007  axlowdimlem16  29011  axlowdimlem17  29012  sizusglecusg  29518  clwlkclwwlkf  30064  imsmetlem  30746  nmoubi  30828  nmobndi  30831  nmounbi  30832  nmlno0lem  30849  nmlnoubi  30852  isblo3i  30857  blometi  30859  blocni  30861  blocn2  30864  ipasslem2  30888  siii  30909  ubthlem1  30926  ubthlem2  30927  ubthlem3  30928  htthlem  30973  hvsubid  31082  hv2times  31117  hi01  31152  hhssabloilem  31317  pjsumi  31766  mayete3i  31784  hoaddcomi  31828  hodsi  31831  hoaddassi  31832  hocadddiri  31835  hocsubdiri  31836  hoaddridi  31842  honegsubi  31852  honegneg  31862  ho2times  31875  eigrei  31890  eigorthi  31893  nmopnegi  32021  hoddii  32045  lnophsi  32057  lnopeqi  32064  nmoptrii  32150  opsqrlem1  32196  opsqrlem6  32201  pjsdii  32211  pjddii  32212  pjscji  32226  pjssposi  32228  pjssdif2i  32230  pjtoi  32235  mdsl2bi  32379  cvmdi  32380  mdslmd3i  32388  mdslmd4i  32389  mdexchi  32391  cvati  32422  cvexchlem  32424  mdsymi  32467  dmdbr5ati  32478  cdj1i  32489  cdj3lem1  32490  xrge0infss  32819  xrge0tsmsd  33134  elrspunidl  33488  2sqr3nconstr  33917  cos9thpinconstrlem2  33926  rrhre  34157  esumpinfval  34209  oms0  34433  eulerpartlems  34496  eulerpartlemgf  34515  probmeasb  34566  acycgr2v  35323  cvmliftlem5  35462  bcneg1  35909  wsuceq3  35988  fullfunfv  36120  finminlem  36491  nn0prpwlem  36495  bj-ceqsalg0  37062  bj-ceqsalgALT  37064  bj-ceqsalgvALT  37066  bj-vtoclgfALT  37233  finxpreclem4  37568  sin2h  37780  cos2h  37781  tan2h  37782  poimirlem1  37791  poimirlem2  37792  poimirlem3  37793  poimirlem4  37794  poimirlem6  37796  poimirlem7  37797  poimirlem11  37801  poimirlem12  37802  poimirlem16  37806  poimirlem17  37807  poimirlem19  37809  poimirlem20  37810  poimirlem23  37813  poimirlem30  37820  poimirlem32  37822  poimir  37823  broucube  37824  mblfinlem1  37827  mblfinlem3  37829  mblfinlem4  37830  ismblfin  37831  volsupnfl  37835  iblmulc2nc  37855  ftc1anc  37871  dvasin  37874  heiborlem3  37983  heiborlem6  37986  heiborlem8  37988  cdleme32fva  40732  isnumbasgrplem1  43380  areaquad  43495  binomcxplemnotnn0  44634  permaxun  45289  fourierdlem101  46488  fourierdlem103  46490  fourierdlem104  46491  sqwvfourb  46510  fourierswlem  46511  fouriersw  46512  m1mod0mod1  47637  sgoldbeven3prm  48066  pgnbgreunbgrlem2lem1  48397  pgnbgreunbgrlem2lem2  48398  pgnbgreunbgrlem2lem3  48399  iooii  49200  aacllem  50083