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  8257  oneo  8505  nnneo  8580  naddcllem  8601  ener  8937  sucdom2  9126  unxpdomlem3  9157  dfac2b  10042  ackbij2  10153  axgroth3  10743  mul02  11313  recreclt  12044  cju  12144  elnnnn0c  12471  elnnz1  12542  uz3m2nn  12833  iccen  13439  mptnn0fsupp  13948  hashgt23el  14375  hashfun  14388  hashf1lem1  14406  hash7g  14437  hash3tpexb  14445  funcnvs2  14864  remim  15068  iseraltlem2  15634  climcndslem1  15803  geo2lim  15829  fprodge0  15947  fprodge1  15949  absefib  16154  efieq1re  16155  3dvds  16289  oddp1d2  16316  bitsres  16431  phiprmpw  16735  pythagtriplem1  16776  symggen  19434  psgnuni  19463  lt6abl  19859  pws1  20293  0ringnnzr  20491  pmatcollpw2lem  22730  uzrest  23850  ressuss  24215  reperflem  24772  xrge0tsms  24788  cphsqrtcl  25139  ovolicopnf  25479  itg2seq  25697  itg2monolem2  25706  itgz  25736  ibl0  25742  iblss  25760  itgeqa  25769  iblconst  25773  iblabsr  25785  iblmulc2  25786  itgsplit  25791  tdeglem4  26013  dvnply2  26241  aannenlem2  26283  aannenlem3  26284  aalioulem2  26287  aaliou3lem2  26297  psercn  26379  abelth  26394  pilem3  26406  resinf1o  26488  efif1olem4  26497  logdivlti  26572  dvlog2lem  26604  efopn  26610  cxpsqrt  26655  isosctrlem1  26770  asinsin  26844  atanlogsub  26868  atanbnd  26878  atantayl2  26890  basellem2  27033  basellem3  27034  isnsqf  27086  ppidif  27114  1sgm2ppw  27151  ppiublem1  27153  bposlem6  27240  bposlem9  27243  gausslemma2dlem1  27317  lgseisenlem1  27326  lgseisen  27330  lgsquad3  27338  m1lgs  27339  ostth3  27589  cutbdaybnd  27775  cutbdaybnd2  27776  cutbdaylt  27778  madebdaylemlrcut  27879  bdayiun  27895  sltsbday  27897  cofcut1  27900  cofcutr  27904  negsproplem4  28011  negsproplem5  28012  negsproplem6  28013  precsexlem11  28197  pw2divscld  28419  pw2divmulsd  28420  pw2divscan2d  28422  pw2divsassd  28423  pw2divsrecd  28427  bdayfinbndlem1  28447  z12zsodd  28462  axlowdimlem3  29001  axlowdimlem7  29005  axlowdimlem16  29014  axlowdim  29018  umgr2v2e  29582  clwlkclwwlken  30070  clwwlken  30110  0wlkonlem2  30177  clwwlknonclwlknonen  30421  dlwwlknondlwlknonen  30424  eulerpartlemgvv  34508  lfuhgr2  35289  poimirlem26  37955  mblfinlem2  37967  itg2addnclem3  37982  pr2cv  43963  isosctrlem1ALT  45348  muldvdsfacgt  47822  fmtnorec1  47988  evengpoap3  48263  pgnioedg1  48572  pgnioedg2  48573  pgnioedg3  48574  pgnioedg4  48575  pgnioedg5  48576  pgnbgreunbgrlem2lem1  48578  pgnbgreunbgrlem2lem2  48579  pgnbgreunbgrlem5lem1  48584  pgnbgreunbgrlem5lem2  48585  pgnbgreunbgrlem5lem3  48586  line2x  49218  icccldii  49382