Theorem mp3an12i 1461

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  oneo  8209  nnneo  8280  ener  8558  unxpdomlem3  8726  dfac2b  9558  ackbij2  9667  axgroth3  10255  mul02  10820  recreclt  11541  cju  11636  elnnnn0c  11945  elnnz1  12011  eluzsubi  12275  uz3m2nn  12294  iccen  12886  mptnn0fsupp  13368  hashgt23el  13788  hashfun  13801  hashf1lem1  13816  funcnvs2  14277  remim  14478  iseraltlem2  15041  climcndslem1  15206  geo2lim  15233  fprodge0  15349  fprodge1  15351  absefib  15553  efieq1re  15554  3dvds  15682  oddp1d2  15709  bitsres  15824  phiprmpw  16115  pythagtriplem1  16155  symggen  18600  psgnuni  18629  lt6abl  19017  pws1  19368  0ringnnzr  20044  pmatcollpw2lem  21387  uzrest  22507  ressuss  22874  reperflem  23428  xrge0tsms  23444  cphsqrtcl  23790  ovolicopnf  24127  itg2seq  24345  itg2monolem2  24354  itgz  24383  ibl0  24389  iblss  24407  itgeqa  24416  iblconst  24420  iblabsr  24432  iblmulc2  24433  itgsplit  24438  tdeglem4  24656  dvnply2  24878  aannenlem2  24920  aannenlem3  24921  aalioulem2  24924  aaliou3lem2  24934  psercn  25016  abelth  25031  pilem3  25043  resinf1o  25122  efif1olem4  25131  logdivlti  25205  dvlog2lem  25237  efopn  25243  cxpsqrt  25288  isosctrlem1  25398  asinsin  25472  atanlogsub  25496  atanbnd  25506  atantayl2  25518  basellem2  25661  basellem3  25662  isnsqf  25714  ppidif  25742  1sgm2ppw  25778  ppiublem1  25780  bposlem6  25867  bposlem9  25870  gausslemma2dlem1  25944  lgseisenlem1  25953  lgseisen  25957  lgsquad3  25965  m1lgs  25966  ostth3  26216  axlowdimlem3  26732  axlowdimlem7  26736  axlowdimlem16  26745  axlowdim  26749  umgr2v2e  27309  clwlkclwwlken  27792  clwwlken  27833  0wlkonlem2  27900  clwwlknonclwlknonen  28144  dlwwlknondlwlknonen  28147  eulerpartlemgvv  31636  lfuhgr2  32367  scutbdaybnd  33277  scutbdaylt  33278  poimirlem26  34920  mblfinlem2  34932  pr2cv  39914  isosctrlem1ALT  41275  fmtnorec1  43706  evengpoap3  43971  line2x  44748