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  8260  oneo  8508  nnneo  8583  naddcllem  8604  ener  8940  sucdom2  9129  unxpdomlem3  9160  dfac2b  10043  ackbij2  10154  axgroth3  10744  mul02  11313  recreclt  12043  cju  12143  elnnnn0c  12448  elnnz1  12519  uz3m2nn  12809  iccen  13415  mptnn0fsupp  13922  hashgt23el  14349  hashfun  14362  hashf1lem1  14380  hash7g  14411  hash3tpexb  14419  funcnvs2  14838  remim  15042  iseraltlem2  15608  climcndslem1  15774  geo2lim  15800  fprodge0  15918  fprodge1  15920  absefib  16125  efieq1re  16126  3dvds  16260  oddp1d2  16287  bitsres  16402  phiprmpw  16705  pythagtriplem1  16746  symggen  19401  psgnuni  19430  lt6abl  19826  pws1  20262  0ringnnzr  20460  pmatcollpw2lem  22723  uzrest  23843  ressuss  24208  reperflem  24765  xrge0tsms  24781  cphsqrtcl  25142  ovolicopnf  25483  itg2seq  25701  itg2monolem2  25710  itgz  25740  ibl0  25746  iblss  25764  itgeqa  25773  iblconst  25777  iblabsr  25789  iblmulc2  25790  itgsplit  25795  tdeglem4  26023  dvnply2  26253  aannenlem2  26295  aannenlem3  26296  aalioulem2  26299  aaliou3lem2  26309  psercn  26394  abelth  26409  pilem3  26421  resinf1o  26503  efif1olem4  26512  logdivlti  26587  dvlog2lem  26619  efopn  26625  cxpsqrt  26670  isosctrlem1  26786  asinsin  26860  atanlogsub  26884  atanbnd  26894  atantayl2  26906  basellem2  27050  basellem3  27051  isnsqf  27103  ppidif  27131  1sgm2ppw  27169  ppiublem1  27171  bposlem6  27258  bposlem9  27261  gausslemma2dlem1  27335  lgseisenlem1  27344  lgseisen  27348  lgsquad3  27356  m1lgs  27357  ostth3  27607  scutbdaybnd  27791  scutbdaybnd2  27792  scutbdaylt  27794  madebdaylemlrcut  27879  bdayiun  27895  ssltbday  27897  cofcut1  27900  cofcutr  27904  negsproplem4  28011  negsproplem5  28012  negsproplem6  28013  precsexlem11  28196  pw2divscld  28416  pw2divsmuld  28417  pw2divscan2d  28419  pw2divsassd  28420  pw2divsrecd  28424  zs12zodd  28459  axlowdimlem3  28998  axlowdimlem7  29002  axlowdimlem16  29011  axlowdim  29015  umgr2v2e  29580  clwlkclwwlken  30068  clwwlken  30108  0wlkonlem2  30175  clwwlknonclwlknonen  30419  dlwwlknondlwlknonen  30422  eulerpartlemgvv  34512  lfuhgr2  35292  poimirlem26  37816  mblfinlem2  37828  itg2addnclem3  37843  pr2cv  43826  isosctrlem1ALT  45211  fmtnorec1  47820  evengpoap3  48082  pgnioedg1  48391  pgnioedg2  48392  pgnioedg3  48393  pgnioedg4  48394  pgnioedg5  48395  pgnbgreunbgrlem2lem1  48397  pgnbgreunbgrlem2lem2  48398  pgnbgreunbgrlem5lem1  48403  pgnbgreunbgrlem5lem2  48404  pgnbgreunbgrlem5lem3  48405  line2x  49037  icccldii  49201