Theorem mp3an12i 1474

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

Syntax hints:   → wi 4   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  csbwrecsg  8262  oneo  8510  nnneo  8585  naddcllem  8606  ener  8942  sucdom2  9131  unxpdomlem3  9162  dfac2b  10048  ackbij2  10159  axgroth3  10749  mul02  11319  recreclt  12050  cju  12150  elnnnn0c  12477  elnnz1  12548  uz3m2nn  12839  iccen  13445  mptnn0fsupp  13954  hashgt23el  14381  hashfun  14394  hashf1lem1  14412  hash7g  14443  hash3tpexb  14451  funcnvs2  14870  remim  15074  iseraltlem2  15640  climcndslem1  15809  geo2lim  15835  fprodge0  15953  fprodge1  15955  absefib  16160  efieq1re  16161  3dvds  16295  oddp1d2  16322  bitsres  16437  phiprmpw  16741  pythagtriplem1  16782  symggen  19440  psgnuni  19469  lt6abl  19865  pws1  20299  0ringnnzr  20501  pmatcollpw2lem  22764  uzrest  23884  ressuss  24249  reperflem  24806  xrge0tsms  24822  cphsqrtcl  25173  ovolicopnf  25513  itg2seq  25731  itg2monolem2  25740  itgz  25770  ibl0  25776  iblss  25794  itgeqa  25803  iblconst  25807  iblabsr  25819  iblmulc2  25820  itgsplit  25825  tdeglem4  26047  dvnply2  26275  aannenlem2  26317  aannenlem3  26318  aalioulem2  26321  aaliou3lem2  26331  psercn  26413  abelth  26428  pilem3  26440  resinf1o  26522  efif1olem4  26531  logdivlti  26606  dvlog2lem  26638  efopn  26644  cxpsqrt  26689  isosctrlem1  26804  asinsin  26878  atanlogsub  26902  atanbnd  26912  atantayl2  26924  basellem2  27067  basellem3  27068  isnsqf  27120  ppidif  27148  1sgm2ppw  27185  ppiublem1  27187  bposlem6  27274  bposlem9  27277  gausslemma2dlem1  27351  lgseisenlem1  27360  lgseisen  27364  lgsquad3  27372  m1lgs  27373  ostth3  27623  cutbdaybnd  27809  cutbdaybnd2  27810  cutbdaylt  27812  madebdaylemlrcut  27913  bdayiun  27929  sltsbday  27931  cofcut1  27934  cofcutr  27938  negsproplem4  28045  negsproplem5  28046  negsproplem6  28047  precsexlem11  28231  pw2divscld  28453  pw2divmulsd  28454  pw2divscan2d  28456  pw2divsassd  28457  pw2divsrecd  28461  bdayfinbndlem1  28481  z12zsodd  28496  axlowdimlem3  29035  axlowdimlem7  29039  axlowdimlem16  29048  axlowdim  29052  umgr2v2e  29616  clwlkclwwlken  30104  clwwlken  30144  0wlkonlem2  30211  clwwlknonclwlknonen  30455  dlwwlknondlwlknonen  30458  eulerpartlemgvv  34572  lfuhgr2  35362  poimirlem26  38028  mblfinlem2  38040  itg2addnclem3  38055  pr2cv  44007  isosctrlem1ALT  45392  muldvdsfacgt  47863  fmtnorec1  48029  evengpoap3  48304  pgnioedg1  48613  pgnioedg2  48614  pgnioedg3  48615  pgnioedg4  48616  pgnioedg5  48617  pgnbgreunbgrlem2lem1  48619  pgnbgreunbgrlem2lem2  48620  pgnbgreunbgrlem5lem1  48625  pgnbgreunbgrlem5lem2  48626  pgnbgreunbgrlem5lem3  48627  line2x  49259  icccldii  49423