Theorem mp3an12i 1468

Description: mp3an 1464 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)

Hypotheses

Ref	Expression
mp3an12i.1	⊢ 𝜑
mp3an12i.2	⊢ 𝜓
mp3an12i.3	⊢ (𝜒 → 𝜃)
mp3an12i.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
mp3an12i	⊢ (𝜒 → 𝜏)

Proof of Theorem mp3an12i

Step	Hyp	Ref	Expression
1		mp3an12i.3	. 2 ⊢ (𝜒 → 𝜃)
2		mp3an12i.1	. . 3 ⊢ 𝜑
3		mp3an12i.2	. . 3 ⊢ 𝜓
4		mp3an12i.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	2, 3, 4	mp3an12 1454	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 17	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:  csbwrecsg  8262  oneo  8510  nnneo  8585  naddcllem  8606  ener  8942  sucdom2  9131  unxpdomlem3  9162  dfac2b  10045  ackbij2  10156  axgroth3  10746  mul02  11315  recreclt  12045  cju  12145  elnnnn0c  12450  elnnz1  12521  uz3m2nn  12811  iccen  13417  mptnn0fsupp  13924  hashgt23el  14351  hashfun  14364  hashf1lem1  14382  hash7g  14413  hash3tpexb  14421  funcnvs2  14840  remim  15044  iseraltlem2  15610  climcndslem1  15776  geo2lim  15802  fprodge0  15920  fprodge1  15922  absefib  16127  efieq1re  16128  3dvds  16262  oddp1d2  16289  bitsres  16404  phiprmpw  16707  pythagtriplem1  16748  symggen  19403  psgnuni  19432  lt6abl  19828  pws1  20264  0ringnnzr  20462  pmatcollpw2lem  22725  uzrest  23845  ressuss  24210  reperflem  24767  xrge0tsms  24783  cphsqrtcl  25144  ovolicopnf  25485  itg2seq  25703  itg2monolem2  25712  itgz  25742  ibl0  25748  iblss  25766  itgeqa  25775  iblconst  25779  iblabsr  25791  iblmulc2  25792  itgsplit  25797  tdeglem4  26025  dvnply2  26255  aannenlem2  26297  aannenlem3  26298  aalioulem2  26301  aaliou3lem2  26311  psercn  26396  abelth  26411  pilem3  26423  resinf1o  26505  efif1olem4  26514  logdivlti  26589  dvlog2lem  26621  efopn  26627  cxpsqrt  26672  isosctrlem1  26788  asinsin  26862  atanlogsub  26886  atanbnd  26896  atantayl2  26908  basellem2  27052  basellem3  27053  isnsqf  27105  ppidif  27133  1sgm2ppw  27171  ppiublem1  27173  bposlem6  27260  bposlem9  27263  gausslemma2dlem1  27337  lgseisenlem1  27346  lgseisen  27350  lgsquad3  27358  m1lgs  27359  ostth3  27609  cutbdaybnd  27795  cutbdaybnd2  27796  cutbdaylt  27798  madebdaylemlrcut  27899  bdayiun  27915  sltsbday  27917  cofcut1  27920  cofcutr  27924  negsproplem4  28031  negsproplem5  28032  negsproplem6  28033  precsexlem11  28217  pw2divscld  28439  pw2divmulsd  28440  pw2divscan2d  28442  pw2divsassd  28443  pw2divsrecd  28447  bdayfinbndlem1  28467  z12zsodd  28482  axlowdimlem3  29021  axlowdimlem7  29025  axlowdimlem16  29034  axlowdim  29038  umgr2v2e  29603  clwlkclwwlken  30091  clwwlken  30131  0wlkonlem2  30198  clwwlknonclwlknonen  30442  dlwwlknondlwlknonen  30445  eulerpartlemgvv  34535  lfuhgr2  35315  poimirlem26  37849  mblfinlem2  37861  itg2addnclem3  37876  pr2cv  43856  isosctrlem1ALT  45241  fmtnorec1  47850  evengpoap3  48112  pgnioedg1  48421  pgnioedg2  48422  pgnioedg3  48423  pgnioedg4  48424  pgnioedg5  48425  pgnbgreunbgrlem2lem1  48427  pgnbgreunbgrlem2lem2  48428  pgnbgreunbgrlem5lem1  48433  pgnbgreunbgrlem5lem2  48434  pgnbgreunbgrlem5lem3  48435  line2x  49067  icccldii  49231