Theorem mp3an12i 1467

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  csbwrecsg  8325  oneo  8598  nnneo  8672  naddcllem  8693  ener  9020  sucdom2  9222  unxpdomlem3  9265  dfac2b  10150  ackbij2  10261  axgroth3  10850  mul02  11418  recreclt  12146  cju  12241  elnnnn0c  12551  elnnz1  12623  eluzsubiOLD  12891  uz3m2nn  12912  iccen  13519  mptnn0fsupp  14020  hashgt23el  14447  hashfun  14460  hashf1lem1  14478  hash7g  14509  hash3tpexb  14517  funcnvs2  14937  remim  15141  iseraltlem2  15704  climcndslem1  15870  geo2lim  15896  fprodge0  16014  fprodge1  16016  absefib  16221  efieq1re  16222  3dvds  16355  oddp1d2  16382  bitsres  16497  phiprmpw  16800  pythagtriplem1  16841  symggen  19456  psgnuni  19485  lt6abl  19881  pws1  20290  0ringnnzr  20490  pmatcollpw2lem  22720  uzrest  23840  ressuss  24206  reperflem  24763  xrge0tsms  24779  cphsqrtcl  25141  ovolicopnf  25482  itg2seq  25700  itg2monolem2  25709  itgz  25739  ibl0  25745  iblss  25763  itgeqa  25772  iblconst  25776  iblabsr  25788  iblmulc2  25789  itgsplit  25794  tdeglem4  26022  dvnply2  26252  aannenlem2  26294  aannenlem3  26295  aalioulem2  26298  aaliou3lem2  26308  psercn  26393  abelth  26408  pilem3  26420  resinf1o  26502  efif1olem4  26511  logdivlti  26586  dvlog2lem  26618  efopn  26624  cxpsqrt  26669  isosctrlem1  26785  asinsin  26859  atanlogsub  26883  atanbnd  26893  atantayl2  26905  basellem2  27049  basellem3  27050  isnsqf  27102  ppidif  27130  1sgm2ppw  27168  ppiublem1  27170  bposlem6  27257  bposlem9  27260  gausslemma2dlem1  27334  lgseisenlem1  27343  lgseisen  27347  lgsquad3  27355  m1lgs  27356  ostth3  27606  scutbdaybnd  27784  scutbdaybnd2  27785  scutbdaylt  27787  madebdaylemlrcut  27867  cofcut1  27885  cofcutr  27889  negsproplem4  27994  negsproplem5  27995  negsproplem6  27996  precsexlem11  28176  pw2divscld  28381  pw2divsmuld  28382  pw2divscan2d  28384  pw2divsrecd  28387  axlowdimlem3  28928  axlowdimlem7  28932  axlowdimlem16  28941  axlowdim  28945  umgr2v2e  29510  clwlkclwwlken  29998  clwwlken  30038  0wlkonlem2  30105  clwwlknonclwlknonen  30349  dlwwlknondlwlknonen  30352  eulerpartlemgvv  34413  lfuhgr2  35146  poimirlem26  37675  mblfinlem2  37687  itg2addnclem3  37702  pr2cv  43539  isosctrlem1ALT  44925  fmtnorec1  47518  evengpoap3  47780  line2x  48701  icccldii  48860