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  3463  brelrn  5886  predeq3  6258  funpr  6543  fvpr1  7136  fvpr2  7137  tfi  7793  peano5  7833  wrecseq3  8256  fpm  8812  0fsupp  9292  ssttrcl  9625  ac6  10391  alephadd  10489  axpre-sup  11081  cnegex2  11317  addlid  11318  renegcli  11444  div0OLD  11832  divclzi  11879  divcan1zi  11880  divcan2zi  11881  divreczi  11882  divcan3zi  11883  divcan4zi  11884  divasszi  11894  divmulzi  11895  divdirzi  11896  redivclzi  11910  ltm1  11986  mulgt1OLD  12003  recgt1i  12042  ltmul1i  12063  ltdiv1i  12064  ltmuldivi  12065  ltmul2i  12066  lemul1i  12067  lemul2i  12068  ledivp1i  12070  ltdivp1i  12071  nnge1  12194  nngt0  12197  nnrecgt0  12209  nnunb  12422  recnz  12593  eluzsubi  12809  ge0gtmnf  13113  x2times  13240  xrub  13253  xrge0neqmnf  13394  1mod  13851  m1expcl2  14036  1exp  14042  expubnd  14129  iexpcyc  14158  expnbnd  14183  expnlbnd  14184  faclbnd4lem1  14244  imval2  15102  cjdivi  15142  resqrex  15201  sqrtneglem  15217  absdivzi  15359  climcndslem1  15803  climcndslem2  15804  fprodge1  15949  bpoly3  16012  sinhval  16110  coshval  16111  ef01bndlem  16140  sin01gt0  16146  cos01gt0  16147  evend2  16315  divalglem5  16355  vdwlem13  16953  prmlem1  17067  prmlem2  17079  ress0  17202  frmdplusg  18811  m1expaddsub  19462  islindf4  21807  resstopn  23139  lecldbas  23172  hmphindis  23750  cnbl0  24726  xrsmopn  24766  zdis  24770  xrhmeo  24901  oprpiece1res1  24906  voliunlem3  25507  volsup  25511  volivth  25562  iblss2  25761  itgss  25767  coeidp  26216  dgrsub  26225  abelth  26394  reeff1olem  26399  sincosq1sgn  26450  sincosq3sgn  26452  sincosq4sgn  26453  sineq0  26476  logdivlt  26573  1cxp  26624  ecxp  26625  sinasin  26841  log2cnv  26896  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  29520  clwlkclwwlkf  30066  imsmetlem  30749  nmoubi  30831  nmobndi  30834  nmounbi  30835  nmlno0lem  30852  nmlnoubi  30855  isblo3i  30860  blometi  30862  blocni  30864  blocn2  30867  ipasslem2  30891  siii  30912  ubthlem1  30929  ubthlem2  30930  ubthlem3  30931  htthlem  30976  hvsubid  31085  hv2times  31120  hi01  31155  hhssabloilem  31320  pjsumi  31769  mayete3i  31787  hoaddcomi  31831  hodsi  31834  hoaddassi  31835  hocadddiri  31838  hocsubdiri  31839  hoaddridi  31845  honegsubi  31855  honegneg  31865  ho2times  31878  eigrei  31893  eigorthi  31896  nmopnegi  32024  hoddii  32048  lnophsi  32060  lnopeqi  32067  nmoptrii  32153  opsqrlem1  32199  opsqrlem6  32204  pjsdii  32214  pjddii  32215  pjscji  32229  pjssposi  32231  pjssdif2i  32233  pjtoi  32238  mdsl2bi  32382  cvmdi  32383  mdslmd3i  32391  mdslmd4i  32392  mdexchi  32394  cvati  32425  cvexchlem  32427  mdsymi  32470  dmdbr5ati  32481  cdj1i  32492  cdj3lem1  32493  xrge0infss  32821  xrge0tsmsd  33122  elrspunidl  33476  2sqr3nconstr  33913  cos9thpinconstrlem2  33922  rrhre  34153  esumpinfval  34205  oms0  34429  eulerpartlems  34492  eulerpartlemgf  34511  probmeasb  34562  acycgr2v  35320  cvmliftlem5  35459  bcneg1  35906  wsuceq3  35985  fullfunfv  36117  finminlem  36488  nn0prpwlem  36492  regsfromunir1  36710  bj-ceqsalg0  37183  bj-ceqsalgALT  37185  bj-ceqsalgvALT  37187  bj-vtoclgfALT  37354  finxpreclem4  37698  sin2h  37919  cos2h  37920  tan2h  37921  poimirlem1  37930  poimirlem2  37931  poimirlem3  37932  poimirlem4  37933  poimirlem6  37935  poimirlem7  37936  poimirlem11  37940  poimirlem12  37941  poimirlem16  37945  poimirlem17  37946  poimirlem19  37948  poimirlem20  37949  poimirlem23  37952  poimirlem30  37959  poimirlem32  37961  poimir  37962  broucube  37963  mblfinlem1  37966  mblfinlem3  37968  mblfinlem4  37969  ismblfin  37970  volsupnfl  37974  iblmulc2nc  37994  ftc1anc  38010  dvasin  38013  heiborlem3  38122  heiborlem6  38125  heiborlem8  38127  cdleme32fva  40871  isnumbasgrplem1  43517  areaquad  43632  binomcxplemnotnn0  44771  permaxun  45426  fourierdlem101  46623  fourierdlem103  46625  fourierdlem104  46626  sqwvfourb  46645  fourierswlem  46646  fouriersw  46647  m1mod0mod1  47796  sgoldbeven3prm  48247  pgnbgreunbgrlem2lem1  48578  pgnbgreunbgrlem2lem2  48579  pgnbgreunbgrlem2lem3  48580  iooii  49381  aacllem  50264