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  5889  predeq3  6261  funpr  6546  fvpr1  7138  fvpr2  7139  tfi  7795  peano5  7835  wrecseq3  8258  fpm  8814  0fsupp  9294  ssttrcl  9625  ac6  10391  alephadd  10489  axpre-sup  11081  cnegex2  11316  addlid  11317  renegcli  11443  div0OLD  11831  divclzi  11877  divcan1zi  11878  divcan2zi  11879  divreczi  11880  divcan3zi  11881  divcan4zi  11882  divasszi  11892  divmulzi  11893  divdirzi  11894  redivclzi  11908  ltm1  11984  mulgt1OLD  12001  recgt1i  12040  ltmul1i  12061  ltdiv1i  12062  ltmuldivi  12063  ltmul2i  12064  lemul1i  12065  lemul2i  12066  ledivp1i  12068  ltdivp1i  12069  nnge1  12174  nngt0  12177  nnrecgt0  12189  nnunb  12398  recnz  12568  eluzsubi  12784  ge0gtmnf  13088  x2times  13215  xrub  13228  xrge0neqmnf  13369  1mod  13824  m1expcl2  14009  1exp  14015  expubnd  14102  iexpcyc  14131  expnbnd  14156  expnlbnd  14157  faclbnd4lem1  14217  imval2  15075  cjdivi  15115  resqrex  15174  sqrtneglem  15190  absdivzi  15332  climcndslem1  15773  climcndslem2  15774  fprodge1  15919  bpoly3  15982  sinhval  16080  coshval  16081  ef01bndlem  16110  sin01gt0  16116  cos01gt0  16117  evend2  16285  divalglem5  16325  vdwlem13  16922  prmlem1  17036  prmlem2  17048  ress0  17171  frmdplusg  18780  m1expaddsub  19431  islindf4  21795  resstopn  23129  lecldbas  23162  hmphindis  23740  cnbl0  24716  xrsmopn  24756  zdis  24760  xrhmeo  24891  oprpiece1res1  24896  voliunlem3  25497  volsup  25501  volivth  25552  iblss2  25751  itgss  25757  coeidp  26209  dgrsub  26218  abelth  26391  reeff1olem  26396  sincosq1sgn  26447  sincosq3sgn  26449  sincosq4sgn  26450  sineq0  26473  logdivlt  26570  1cxp  26621  ecxp  26622  sinasin  26839  log2cnv  26894  efexple  27232  bposlem8  27242  lgsdir2lem2  27277  2sqb  27383  eqcuts2  27766  cutsun12  27770  eucliddivs  28356  pw2cut  28440  axpaschlem  28997  axlowdimlem9  29007  axlowdimlem12  29010  axlowdimlem16  29014  axlowdimlem17  29015  sizusglecusg  29521  clwlkclwwlkf  30067  imsmetlem  30750  nmoubi  30832  nmobndi  30835  nmounbi  30836  nmlno0lem  30853  nmlnoubi  30856  isblo3i  30861  blometi  30863  blocni  30865  blocn2  30868  ipasslem2  30892  siii  30913  ubthlem1  30930  ubthlem2  30931  ubthlem3  30932  htthlem  30977  hvsubid  31086  hv2times  31121  hi01  31156  hhssabloilem  31321  pjsumi  31770  mayete3i  31788  hoaddcomi  31832  hodsi  31835  hoaddassi  31836  hocadddiri  31839  hocsubdiri  31840  hoaddridi  31846  honegsubi  31856  honegneg  31866  ho2times  31879  eigrei  31894  eigorthi  31897  nmopnegi  32025  hoddii  32049  lnophsi  32061  lnopeqi  32068  nmoptrii  32154  opsqrlem1  32200  opsqrlem6  32205  pjsdii  32215  pjddii  32216  pjscji  32230  pjssposi  32232  pjssdif2i  32234  pjtoi  32239  mdsl2bi  32383  cvmdi  32384  mdslmd3i  32392  mdslmd4i  32393  mdexchi  32395  cvati  32426  cvexchlem  32428  mdsymi  32471  dmdbr5ati  32482  cdj1i  32493  cdj3lem1  32494  xrge0infss  32823  xrge0tsmsd  33139  elrspunidl  33493  2sqr3nconstr  33931  cos9thpinconstrlem2  33940  rrhre  34171  esumpinfval  34223  oms0  34447  eulerpartlems  34510  eulerpartlemgf  34529  probmeasb  34580  acycgr2v  35338  cvmliftlem5  35477  bcneg1  35924  wsuceq3  36003  fullfunfv  36135  finminlem  36506  nn0prpwlem  36510  regsfromunir1  36728  bj-ceqsalg0  37193  bj-ceqsalgALT  37195  bj-ceqsalgvALT  37197  bj-vtoclgfALT  37364  finxpreclem4  37706  sin2h  37922  cos2h  37923  tan2h  37924  poimirlem1  37933  poimirlem2  37934  poimirlem3  37935  poimirlem4  37936  poimirlem6  37938  poimirlem7  37939  poimirlem11  37943  poimirlem12  37944  poimirlem16  37948  poimirlem17  37949  poimirlem19  37951  poimirlem20  37952  poimirlem23  37955  poimirlem30  37962  poimirlem32  37964  poimir  37965  broucube  37966  mblfinlem1  37969  mblfinlem3  37971  mblfinlem4  37972  ismblfin  37973  volsupnfl  37977  iblmulc2nc  37997  ftc1anc  38013  dvasin  38016  heiborlem3  38125  heiborlem6  38128  heiborlem8  38130  cdleme32fva  40874  isnumbasgrplem1  43532  areaquad  43647  binomcxplemnotnn0  44786  permaxun  45441  fourierdlem101  46639  fourierdlem103  46641  fourierdlem104  46642  sqwvfourb  46661  fourierswlem  46662  fouriersw  46663  m1mod0mod1  47788  sgoldbeven3prm  48217  pgnbgreunbgrlem2lem1  48548  pgnbgreunbgrlem2lem2  48549  pgnbgreunbgrlem2lem3  48550  iooii  49351  aacllem  50234