Theorem mp3an12i 1467

Description: mp3an 1463 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 1453	. 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  8274  oneo  8522  nnneo  8596  naddcllem  8617  ener  8949  sucdom2  9144  unxpdomlem3  9175  dfac2b  10062  ackbij2  10173  axgroth3  10762  mul02  11330  recreclt  12060  cju  12160  elnnnn0c  12465  elnnz1  12537  eluzsubiOLD  12805  uz3m2nn  12831  iccen  13436  mptnn0fsupp  13940  hashgt23el  14367  hashfun  14380  hashf1lem1  14398  hash7g  14429  hash3tpexb  14437  funcnvs2  14856  remim  15060  iseraltlem2  15626  climcndslem1  15792  geo2lim  15818  fprodge0  15936  fprodge1  15938  absefib  16143  efieq1re  16144  3dvds  16278  oddp1d2  16305  bitsres  16420  phiprmpw  16723  pythagtriplem1  16764  symggen  19385  psgnuni  19414  lt6abl  19810  pws1  20246  0ringnnzr  20446  pmatcollpw2lem  22698  uzrest  23818  ressuss  24184  reperflem  24741  xrge0tsms  24757  cphsqrtcl  25118  ovolicopnf  25459  itg2seq  25677  itg2monolem2  25686  itgz  25716  ibl0  25722  iblss  25740  itgeqa  25749  iblconst  25753  iblabsr  25765  iblmulc2  25766  itgsplit  25771  tdeglem4  25999  dvnply2  26229  aannenlem2  26271  aannenlem3  26272  aalioulem2  26275  aaliou3lem2  26285  psercn  26370  abelth  26385  pilem3  26397  resinf1o  26479  efif1olem4  26488  logdivlti  26563  dvlog2lem  26595  efopn  26601  cxpsqrt  26646  isosctrlem1  26762  asinsin  26836  atanlogsub  26860  atanbnd  26870  atantayl2  26882  basellem2  27026  basellem3  27027  isnsqf  27079  ppidif  27107  1sgm2ppw  27145  ppiublem1  27147  bposlem6  27234  bposlem9  27237  gausslemma2dlem1  27311  lgseisenlem1  27320  lgseisen  27324  lgsquad3  27332  m1lgs  27333  ostth3  27583  scutbdaybnd  27762  scutbdaybnd2  27763  scutbdaylt  27765  madebdaylemlrcut  27849  bdayiun  27865  cofcut1  27869  cofcutr  27873  negsproplem4  27978  negsproplem5  27979  negsproplem6  27980  precsexlem11  28160  pw2divscld  28367  pw2divsmuld  28368  pw2divscan2d  28370  pw2divsassd  28371  pw2divsrecd  28375  zs12zodd  28395  axlowdimlem3  28925  axlowdimlem7  28929  axlowdimlem16  28938  axlowdim  28942  umgr2v2e  29507  clwlkclwwlken  29992  clwwlken  30032  0wlkonlem2  30099  clwwlknonclwlknonen  30343  dlwwlknondlwlknonen  30346  eulerpartlemgvv  34361  lfuhgr2  35100  poimirlem26  37634  mblfinlem2  37646  itg2addnclem3  37661  pr2cv  43531  isosctrlem1ALT  44917  fmtnorec1  47532  evengpoap3  47794  pgnioedg1  48092  pgnioedg2  48093  pgnioedg3  48094  pgnioedg4  48095  pgnioedg5  48096  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem5lem1  48104  pgnbgreunbgrlem5lem2  48105  pgnbgreunbgrlem5lem3  48106  line2x  48737  icccldii  48901