Theorem mp3an12i 1464

Description: mp3an 1460 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 1450	. 2 ⊢ (𝜃 → 𝜏)
6	1, 5	syl 17	1 ⊢ (𝜒 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  csbwrecsg  8345  oneo  8618  nnneo  8692  naddcllem  8713  ener  9040  sucdom2  9241  unxpdomlem3  9286  dfac2b  10169  ackbij2  10280  axgroth3  10869  mul02  11437  recreclt  12165  cju  12260  elnnnn0c  12569  elnnz1  12641  eluzsubiOLD  12910  uz3m2nn  12931  iccen  13534  mptnn0fsupp  14035  hashgt23el  14460  hashfun  14473  hashf1lem1  14491  hash7g  14522  hash3tpexb  14530  funcnvs2  14949  remim  15153  iseraltlem2  15716  climcndslem1  15882  geo2lim  15908  fprodge0  16026  fprodge1  16028  absefib  16231  efieq1re  16232  3dvds  16365  oddp1d2  16392  bitsres  16507  phiprmpw  16810  pythagtriplem1  16850  symggen  19503  psgnuni  19532  lt6abl  19928  pws1  20339  0ringnnzr  20542  pmatcollpw2lem  22799  uzrest  23921  ressuss  24287  reperflem  24854  xrge0tsms  24870  cphsqrtcl  25232  ovolicopnf  25573  itg2seq  25792  itg2monolem2  25801  itgz  25831  ibl0  25837  iblss  25855  itgeqa  25864  iblconst  25868  iblabsr  25880  iblmulc2  25881  itgsplit  25886  tdeglem4  26114  dvnply2  26344  aannenlem2  26386  aannenlem3  26387  aalioulem2  26390  aaliou3lem2  26400  psercn  26485  abelth  26500  pilem3  26512  resinf1o  26593  efif1olem4  26602  logdivlti  26677  dvlog2lem  26709  efopn  26715  cxpsqrt  26760  isosctrlem1  26876  asinsin  26950  atanlogsub  26974  atanbnd  26984  atantayl2  26996  basellem2  27140  basellem3  27141  isnsqf  27193  ppidif  27221  1sgm2ppw  27259  ppiublem1  27261  bposlem6  27348  bposlem9  27351  gausslemma2dlem1  27425  lgseisenlem1  27434  lgseisen  27438  lgsquad3  27446  m1lgs  27447  ostth3  27697  scutbdaybnd  27875  scutbdaybnd2  27876  scutbdaylt  27878  madebdaylemlrcut  27952  cofcut1  27969  cofcutr  27973  negsproplem4  28078  negsproplem5  28079  negsproplem6  28080  precsexlem11  28256  axlowdimlem3  28974  axlowdimlem7  28978  axlowdimlem16  28987  axlowdim  28991  umgr2v2e  29558  clwlkclwwlken  30041  clwwlken  30081  0wlkonlem2  30148  clwwlknonclwlknonen  30392  dlwwlknondlwlknonen  30395  eulerpartlemgvv  34358  lfuhgr2  35103  poimirlem26  37633  mblfinlem2  37645  itg2addnclem3  37660  pr2cv  43538  isosctrlem1ALT  44932  fmtnorec1  47462  evengpoap3  47724  line2x  48604  icccldii  48715