Theorem mp3an12i 1495

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  csbwrecsg  8361  oneo  8614  nnneo  8689  naddcllem  8710  ener  9053  sucdom2  9243  unxpdomlem3  9274  dfac2b  10233  ackbij2  10344  axgroth3  10940  mul02  11512  recreclt  12240  cju  12340  elnnnn0c  12675  elnnz1  12746  uz3m2nn  13045  iccen  13652  mptnn0fsupp  14164  hashgt23el  14593  hashfun  14606  hashf1lem1  14624  hash7g  14655  hash3tpexb  14663  funcnvs2  15090  remim  15310  iseraltlem2  15876  climcndslem1  16044  geo2lim  16070  fprodge0  16186  fprodge1  16188  absefib  16392  efieq1re  16393  3dvds  16527  oddp1d2  16554  bitsres  16669  phiprmpw  16979  pythagtriplem1  17020  symggen  19711  psgnuni  19740  lt6abl  20136  pws1  20581  0ringnnzr  20803  pmatcollpw2lem  23122  uzrest  24243  ressuss  24608  reperflem  25165  xrge0tsms  25181  cphsqrtcl  25532  ovolicopnf  25872  itg2seq  26090  itg2monolem2  26099  itgz  26128  ibl0  26134  iblss  26152  itgeqa  26161  iblconst  26165  iblabsr  26177  iblmulc2  26178  itgsplit  26183  tdeglem4  26405  dvnply2  26635  aannenlem2  26683  aannenlem3  26684  aalioulem2  26687  aaliou3lem2  26697  psercn  26780  abelth  26795  pilem3  26807  resinf1o  26891  efif1olem4  26900  logdivlti  26975  dvlog2lem  27007  efopn  27013  cxpsqrt  27058  isosctrlem1  27173  asinsin  27247  atanlogsub  27271  atanbnd  27281  atantayl2  27293  basellem2  27436  basellem3  27437  isnsqf  27489  ppidif  27517  1sgm2ppw  27554  ppiublem1  27556  bposlem6  27643  bposlem9  27646  gausslemma2dlem1  27720  lgseisenlem1  27729  lgseisen  27733  lgsquad3  27741  m1lgs  27742  ostth3  27992  fltoprmlem2  28021  cutbdaybnd  28208  cutbdaybnd2  28209  cutbdaylt  28211  madebdaylemlrcut  28312  bdayiun  28328  sltsbday  28330  cofcut1  28333  cofcutr  28337  negsproplem4  28444  negsproplem5  28445  negsproplem6  28446  precsexlem11  28630  pw2divscld  28852  pw2divmulsd  28853  pw2divscan2d  28855  pw2divsassd  28856  pw2divsrecd  28860  bdayfinbndlem1  28880  z12zsodd  28895  axlowdimlem3  29549  axlowdimlem7  29553  axlowdimlem16  29562  axlowdim  29566  lfuhgr2  29754  umgr2v2e  30133  wlkiswwlksupgr2  30493  clwlkclwwlken  30630  clwwlken  30670  0wlkonlem2  30737  clwwlknonclwlknonen  30991  dlwwlknondlwlknonen  30994  eulerpartlemgvv  35075  ptpconn  36164  nmulprop  37116  poimirlem26  38755  mblfinlem2  38767  itg2addnclem3  38782  pr2cv  44739  isosctrlem1ALT  46105  fourierdlem48  47367  fourierdlem49  47368  fourierdlem113  47432  muldvdsfacgt  48659  fmtnorec1  48825  evengpoap3  49100  pgnioedg1  49409  pgnioedg2  49410  pgnioedg3  49411  pgnioedg4  49412  pgnioedg5  49413  pgnbgreunbgrlem2lem1  49415  pgnbgreunbgrlem2lem2  49416  pgnbgreunbgrlem5lem1  49421  pgnbgreunbgrlem5lem2  49422  pgnbgreunbgrlem5lem3  49423  icccldii  50236