Theorem mp3an12 1478

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mp3an12i  1492  ceqsalg  3488  brelrn  5932  predeq3  6306  funpr  6592  fvpr1  7190  fvpr2  7191  tfi  7848  peano5  7889  wrecseq3  8313  fpm  8872  0fsupp  9349  ssttrcl  9683  ac6  10463  alephadd  10561  axpre-sup  11153  cnegex2  11391  addlid  11392  renegcli  11518  divclzi  11949  divcan1zi  11950  divcan2zi  11951  divreczi  11952  divcan3zi  11953  divcan4zi  11954  divasszi  11964  divmulzi  11965  divdirzi  11966  redivclzi  11980  ltm1  12056  recgt1i  12111  ltmul1i  12132  ltdiv1i  12133  ltmuldivi  12134  ltmul2i  12135  lemul1i  12136  lemul2i  12137  ledivp1i  12139  ltdivp1i  12140  nnge1  12263  nngt0  12266  nnrecgt0  12278  nnunb  12499  recnz  12670  eluzsubi  12893  ge0gtmnf  13197  x2times  13324  xrub  13337  xrge0neqmnf  13478  1mod  13935  m1expcl2  14120  1exp  14126  expubnd  14213  iexpcyc  14242  expnbnd  14267  expnlbnd  14268  faclbnd4lem1  14328  imval2  15201  cjdivi  15241  resqrex  15300  sqrtneglem  15316  absdivzi  15458  climcndslem1  15902  climcndslem2  15903  fprodge1  16048  bpoly3  16111  sinhval  16209  coshval  16210  ef01bndlem  16239  sin01gt0  16245  cos01gt0  16246  evend2  16414  divalglem5  16454  vdwlem13  17052  prmlem1  17166  prmlem2  17179  ress0  17302  frmdplusg  18912  m1expaddsub  19567  islindf4  21967  resstopn  23322  lecldbas  23355  hmphindis  23933  cnbl0  24909  xrsmopn  24949  zdis  24953  xrhmeo  25084  oprpiece1res1  25089  voliunlem3  25690  volsup  25694  volivth  25745  iblss2  25944  itgss  25950  coeidp  26399  dgrsub  26408  abelth  26580  reeff1olem  26585  sincosq1sgn  26639  sincosq3sgn  26641  sincosq4sgn  26642  sineq0  26665  logdivlt  26762  1cxp  26813  ecxp  26814  sinasin  27030  log2cnv  27085  efexple  27421  bposlem8  27431  lgsdir2lem2  27466  2sqb  27572  eqcuts2  27955  cutsun12  27959  eucliddivs  28545  pw2cut  28629  axpaschlem  29256  axlowdimlem9  29266  axlowdimlem12  29269  axlowdimlem16  29273  axlowdimlem17  29274  sizusglecusg  29779  clwlkclwwlkf  30325  imsmetlem  31008  nmoubi  31090  nmobndi  31093  nmounbi  31094  nmlno0lem  31111  nmlnoubi  31114  isblo3i  31119  blometi  31121  blocni  31123  blocn2  31126  ipasslem2  31150  siii  31171  ubthlem1  31188  ubthlem2  31189  ubthlem3  31190  htthlem  31235  hvsubid  31344  hv2times  31379  hi01  31414  hhssabloilem  31579  pjsumi  32028  mayete3i  32046  hoaddcomi  32090  hodsi  32093  hoaddassi  32094  hocadddiri  32097  hocsubdiri  32098  hoaddridi  32104  honegsubi  32114  honegneg  32124  ho2times  32137  eigrei  32152  eigorthi  32155  nmopnegi  32283  hoddii  32307  lnophsi  32319  lnopeqi  32326  nmoptrii  32412  opsqrlem1  32458  opsqrlem6  32463  pjsdii  32473  pjddii  32474  pjscji  32488  pjssposi  32490  pjssdif2i  32492  pjtoi  32497  mdsl2bi  32641  cvmdi  32642  mdslmd3i  32650  mdslmd4i  32651  mdexchi  32653  cvati  32684  cvexchlem  32686  mdsymi  32729  dmdbr5ati  32740  cdj1i  32751  cdj3lem1  32752  xrge0infss  33071  xrge0tsmsd  33359  elrspunidl  33702  2sqr3nconstr  34137  cos9thpinconstrlem2  34146  rrhre  34377  esumpinfval  34429  oms0  34653  eulerpartlems  34716  eulerpartlemgf  34735  probmeasb  34786  acycgr2v  35596  cvmliftlem5  35735  bcneg1  36182  wsuceq3  36261  fullfunfv  36393  finminlem  36773  nn0prpwlem  36777  regsfromunir1  36995  bj-ceqsalg0  37467  bj-ceqsalgALT  37469  bj-ceqsalgvALT  37471  bj-vtoclgfALT  37639  finxpreclem4  37984  sin2h  38205  cos2h  38206  tan2h  38207  poimirlem1  38216  poimirlem2  38217  poimirlem3  38218  poimirlem4  38219  poimirlem6  38221  poimirlem7  38222  poimirlem11  38226  poimirlem12  38227  poimirlem16  38231  poimirlem17  38232  poimirlem19  38234  poimirlem20  38235  poimirlem23  38238  poimirlem30  38245  poimirlem32  38247  poimir  38248  broucube  38249  mblfinlem1  38252  mblfinlem3  38254  mblfinlem4  38255  ismblfin  38256  volsupnfl  38260  iblmulc2nc  38280  ftc1anc  38296  dvasin  38299  heiborlem3  38408  heiborlem6  38411  heiborlem8  38413  cdleme32fva  41157  isnumbasgrplem1  43776  areaquad  43891  binomcxplemnotnn0  45014  permaxun  45668  fourierdlem101  46869  fourierdlem103  46871  fourierdlem104  46872  sqwvfourb  46891  fourierswlem  46892  fouriersw  46893  m1mod0mod1  48042  sgoldbeven3prm  48493  pgnbgreunbgrlem2lem1  48824  pgnbgreunbgrlem2lem2  48825  pgnbgreunbgrlem2lem3  48826  iooii  49641  aacllem  50546