Theorem 3adantl3 1166

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3adantl.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adantl3	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl3

Step	Hyp	Ref	Expression
1		3simpa 1146	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 579	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  dif1ennnALT  9301  infpssrlem4  10329  fin23lem11  10340  tskwun  10807  gruf  10834  lediv2a  12138  prunioo  13490  nn0p1elfzo  13707  hashunsnggt  14385  rpnnen2lem7  16196  muldvds1  16257  muldvds2  16258  dvdscmul  16259  dvdsmulc  16260  rpexp  16693  pospropd  18318  mdetmul  22524  elcls  22976  iscnp4  23166  cnpnei  23167  cnpflf2  23903  cnpflf  23904  cnpfcf  23944  xbln0  24319  blcls  24414  iimulcl  24859  icccvx  24874  iscau2  25204  rrxcph  25319  cncombf  25586  mumul  27112  noetalem1  27673  ax5seglem1  28738  ax5seglem2  28739  wwlksnext  29703  clwwlkinwwlk  29849  nvmul0or  30459  fh1  31427  fh2  31428  cm2j  31429  pjoi0  31526  hoadddi  31612  hmopco  31832  padct  32501  iocinif  32549  volfiniune  33849  eulerpartlemb  33988  ivthALT  35819  lindsadd  37086  cnambfre  37141  rngohomco  37447  rngoisoco  37455  pexmidlem3N  39445  hdmapglem7  41402  sticksstones12a  41629  factwoffsmonot  41694  relexpmulg  43140  supxrgere  44715  supxrgelem  44719  supxrge  44720  infxr  44749  infleinflem2  44753  rexabslelem  44800  pimxrneun  44871  lptre2pt  45028  fnlimfvre  45062  limsupmnfuzlem  45114  climisp  45134  limsupgtlem  45165  dvnprodlem1  45334  ibliccsinexp  45339  iblioosinexp  45341  fourierdlem12  45507  fourierdlem41  45536  fourierdlem42  45537  fourierdlem48  45542  fourierdlem49  45543  fourierdlem51  45545  fourierdlem73  45567  fourierdlem74  45568  fourierdlem75  45569  fourierdlem97  45591  etransclem24  45646  ioorrnopnlem  45692  issalnnd  45733  sge0rpcpnf  45809  sge0seq  45834  meaiuninc3v  45872  smfmullem4  46182  smflimsupmpt  46217  smfliminfmpt  46220  lincdifsn  47492