Theorem mp3an12i 1491

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  csbwrecsg  8315  oneo  8566  nnneo  8641  naddcllem  8662  ener  8998  sucdom2  9187  unxpdomlem3  9218  dfac2b  10114  ackbij2  10225  axgroth3  10816  mul02  11388  recreclt  12114  cju  12214  elnnnn0c  12549  elnnz1  12620  uz3m2nn  12918  iccen  13524  mptnn0fsupp  14033  hashgt23el  14461  hashfun  14474  hashf1lem1  14492  hash7g  14523  hash3tpexb  14531  funcnvs2  14950  remim  15168  iseraltlem2  15734  climcndslem1  15903  geo2lim  15929  fprodge0  16047  fprodge1  16049  absefib  16254  efieq1re  16255  3dvds  16389  oddp1d2  16416  bitsres  16531  phiprmpw  16835  pythagtriplem1  16876  symggen  19540  psgnuni  19569  lt6abl  19965  pws1  20406  0ringnnzr  20609  pmatcollpw2lem  22903  uzrest  24023  ressuss  24388  reperflem  24945  xrge0tsms  24961  cphsqrtcl  25312  ovolicopnf  25652  itg2seq  25870  itg2monolem2  25879  itgz  25909  ibl0  25915  iblss  25933  itgeqa  25942  iblconst  25946  iblabsr  25958  iblmulc2  25959  itgsplit  25964  tdeglem4  26186  dvnply2  26417  aannenlem2  26459  aannenlem3  26460  aalioulem2  26463  aaliou3lem2  26473  psercn  26555  abelth  26570  pilem3  26582  resinf1o  26667  efif1olem4  26676  logdivlti  26751  dvlog2lem  26783  efopn  26789  cxpsqrt  26834  isosctrlem1  26949  asinsin  27023  atanlogsub  27047  atanbnd  27057  atantayl2  27069  basellem2  27212  basellem3  27213  isnsqf  27265  ppidif  27293  1sgm2ppw  27330  ppiublem1  27332  bposlem6  27419  bposlem9  27422  gausslemma2dlem1  27496  lgseisenlem1  27505  lgseisen  27509  lgsquad3  27517  m1lgs  27518  ostth3  27768  cutbdaybnd  27954  cutbdaybnd2  27955  cutbdaylt  27957  madebdaylemlrcut  28058  bdayiun  28074  sltsbday  28076  cofcut1  28079  cofcutr  28083  negsproplem4  28190  negsproplem5  28191  negsproplem6  28192  precsexlem11  28376  pw2divscld  28598  pw2divmulsd  28599  pw2divscan2d  28601  pw2divsassd  28602  pw2divsrecd  28606  bdayfinbndlem1  28626  z12zsodd  28641  axlowdimlem3  29235  axlowdimlem7  29239  axlowdimlem16  29248  axlowdim  29252  umgr2v2e  29816  clwlkclwwlken  30304  clwwlken  30344  0wlkonlem2  30411  clwwlknonclwlknonen  30655  dlwwlknondlwlknonen  30658  eulerpartlemgvv  34711  lfuhgr2  35544  nmulprop  36615  poimirlem26  38220  mblfinlem2  38232  itg2addnclem3  38247  pr2cv  44201  isosctrlem1ALT  45569  fourierdlem48  46795  fourierdlem49  46796  fourierdlem113  46860  muldvdsfacgt  48047  fmtnorec1  48213  evengpoap3  48488  pgnioedg1  48797  pgnioedg2  48798  pgnioedg3  48799  pgnioedg4  48800  pgnioedg5  48801  pgnbgreunbgrlem2lem1  48803  pgnbgreunbgrlem2lem2  48804  pgnbgreunbgrlem5lem1  48809  pgnbgreunbgrlem5lem2  48810  pgnbgreunbgrlem5lem3  48811  line2x  49454  icccldii  49617