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  8265  oneo  8513  nnneo  8588  naddcllem  8609  ener  8945  sucdom2  9134  unxpdomlem3  9165  dfac2b  10050  ackbij2  10161  axgroth3  10751  mul02  11321  recreclt  12052  cju  12152  elnnnn0c  12479  elnnz1  12550  uz3m2nn  12841  iccen  13447  mptnn0fsupp  13956  hashgt23el  14383  hashfun  14396  hashf1lem1  14414  hash7g  14445  hash3tpexb  14453  funcnvs2  14872  remim  15076  iseraltlem2  15642  climcndslem1  15811  geo2lim  15837  fprodge0  15955  fprodge1  15957  absefib  16162  efieq1re  16163  3dvds  16297  oddp1d2  16324  bitsres  16439  phiprmpw  16743  pythagtriplem1  16784  symggen  19442  psgnuni  19471  lt6abl  19867  pws1  20301  0ringnnzr  20499  pmatcollpw2lem  22758  uzrest  23878  ressuss  24243  reperflem  24800  xrge0tsms  24816  cphsqrtcl  25167  ovolicopnf  25507  itg2seq  25725  itg2monolem2  25734  itgz  25764  ibl0  25770  iblss  25788  itgeqa  25797  iblconst  25801  iblabsr  25813  iblmulc2  25814  itgsplit  25819  tdeglem4  26041  dvnply2  26270  aannenlem2  26312  aannenlem3  26313  aalioulem2  26316  aaliou3lem2  26326  psercn  26410  abelth  26425  pilem3  26437  resinf1o  26519  efif1olem4  26528  logdivlti  26603  dvlog2lem  26635  efopn  26641  cxpsqrt  26686  isosctrlem1  26801  asinsin  26875  atanlogsub  26899  atanbnd  26909  atantayl2  26921  basellem2  27065  basellem3  27066  isnsqf  27118  ppidif  27146  1sgm2ppw  27183  ppiublem1  27185  bposlem6  27272  bposlem9  27275  gausslemma2dlem1  27349  lgseisenlem1  27358  lgseisen  27362  lgsquad3  27370  m1lgs  27371  ostth3  27621  cutbdaybnd  27807  cutbdaybnd2  27808  cutbdaylt  27810  madebdaylemlrcut  27911  bdayiun  27927  sltsbday  27929  cofcut1  27932  cofcutr  27936  negsproplem4  28043  negsproplem5  28044  negsproplem6  28045  precsexlem11  28229  pw2divscld  28451  pw2divmulsd  28452  pw2divscan2d  28454  pw2divsassd  28455  pw2divsrecd  28459  bdayfinbndlem1  28479  z12zsodd  28494  axlowdimlem3  29033  axlowdimlem7  29037  axlowdimlem16  29046  axlowdim  29050  umgr2v2e  29615  clwlkclwwlken  30103  clwwlken  30143  0wlkonlem2  30210  clwwlknonclwlknonen  30454  dlwwlknondlwlknonen  30457  eulerpartlemgvv  34542  lfuhgr2  35323  poimirlem26  37989  mblfinlem2  38001  itg2addnclem3  38016  pr2cv  44001  isosctrlem1ALT  45386  muldvdsfacgt  47854  fmtnorec1  48020  evengpoap3  48295  pgnioedg1  48604  pgnioedg2  48605  pgnioedg3  48606  pgnioedg4  48607  pgnioedg5  48608  pgnbgreunbgrlem2lem1  48610  pgnbgreunbgrlem2lem2  48611  pgnbgreunbgrlem5lem1  48616  pgnbgreunbgrlem5lem2  48617  pgnbgreunbgrlem5lem3  48618  line2x  49250  icccldii  49414