Theorem mp3an12i 1465

Description: mp3an 1461 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 1451	. 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  csbwrecsg  8302  oneo  8577  nnneo  8650  naddcllem  8671  ener  8993  sucdom2  9202  unxpdomlem3  9248  dfac2b  10121  ackbij2  10234  axgroth3  10822  mul02  11388  recreclt  12109  cju  12204  elnnnn0c  12513  elnnz1  12584  eluzsubiOLD  12852  uz3m2nn  12871  iccen  13470  mptnn0fsupp  13958  hashgt23el  14380  hashfun  14393  hashf1lem1  14411  hashf1lem1OLD  14412  funcnvs2  14860  remim  15060  iseraltlem2  15625  climcndslem1  15791  geo2lim  15817  fprodge0  15933  fprodge1  15935  absefib  16137  efieq1re  16138  3dvds  16270  oddp1d2  16297  bitsres  16410  phiprmpw  16705  pythagtriplem1  16745  symggen  19332  psgnuni  19361  lt6abl  19757  pws1  20131  0ringnnzr  20294  pmatcollpw2lem  22270  uzrest  23392  ressuss  23758  reperflem  24325  xrge0tsms  24341  cphsqrtcl  24692  ovolicopnf  25032  itg2seq  25251  itg2monolem2  25260  itgz  25289  ibl0  25295  iblss  25313  itgeqa  25322  iblconst  25326  iblabsr  25338  iblmulc2  25339  itgsplit  25344  tdeglem4  25568  tdeglem4OLD  25569  dvnply2  25791  aannenlem2  25833  aannenlem3  25834  aalioulem2  25837  aaliou3lem2  25847  psercn  25929  abelth  25944  pilem3  25956  resinf1o  26036  efif1olem4  26045  logdivlti  26119  dvlog2lem  26151  efopn  26157  cxpsqrt  26202  isosctrlem1  26312  asinsin  26386  atanlogsub  26410  atanbnd  26420  atantayl2  26432  basellem2  26575  basellem3  26576  isnsqf  26628  ppidif  26656  1sgm2ppw  26692  ppiublem1  26694  bposlem6  26781  bposlem9  26784  gausslemma2dlem1  26858  lgseisenlem1  26867  lgseisen  26871  lgsquad3  26879  m1lgs  26880  ostth3  27130  scutbdaybnd  27305  scutbdaybnd2  27306  scutbdaylt  27308  madebdaylemlrcut  27382  cofcut1  27396  cofcutr  27400  negsproplem4  27494  negsproplem5  27495  negsproplem6  27496  precsexlem11  27652  axlowdimlem3  28191  axlowdimlem7  28195  axlowdimlem16  28204  axlowdim  28208  umgr2v2e  28771  clwlkclwwlken  29254  clwwlken  29294  0wlkonlem2  29361  clwwlknonclwlknonen  29605  dlwwlknondlwlknonen  29608  eulerpartlemgvv  33363  lfuhgr2  34097  poimirlem26  36502  mblfinlem2  36514  itg2addnclem3  36529  pr2cv  42284  isosctrlem1ALT  43680  fmtnorec1  46191  evengpoap3  46453  line2x  47393  icccldii  47504