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 578	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  dif1ennnALT  9279  infpssrlem4  10303  fin23lem11  10314  tskwun  10781  gruf  10808  lediv2a  12112  prunioo  13462  nn0p1elfzo  13679  hashunsnggt  14358  rpnnen2lem7  16167  muldvds1  16228  muldvds2  16229  dvdscmul  16230  dvdsmulc  16231  rpexp  16663  pospropd  18284  mdetmul  22345  elcls  22797  iscnp4  22987  cnpnei  22988  cnpflf2  23724  cnpflf  23725  cnpfcf  23765  xbln0  24140  blcls  24235  iimulcl  24680  icccvx  24695  iscau2  25025  rrxcph  25140  cncombf  25407  mumul  26921  noetalem1  27480  ax5seglem1  28453  ax5seglem2  28454  wwlksnext  29414  clwwlkinwwlk  29560  nvmul0or  30170  fh1  31138  fh2  31139  cm2j  31140  pjoi0  31237  hoadddi  31323  hmopco  31543  padct  32211  iocinif  32259  volfiniune  33526  eulerpartlemb  33665  ivthALT  35523  lindsadd  36784  cnambfre  36839  rngohomco  37145  rngoisoco  37153  pexmidlem3N  39146  hdmapglem7  41103  sticksstones12a  41279  factwoffsmonot  41329  relexpmulg  42763  supxrgere  44341  supxrgelem  44345  supxrge  44346  infxr  44375  infleinflem2  44379  rexabslelem  44426  pimxrneun  44497  lptre2pt  44654  fnlimfvre  44688  limsupmnfuzlem  44740  climisp  44760  limsupgtlem  44791  dvnprodlem1  44960  ibliccsinexp  44965  iblioosinexp  44967  fourierdlem12  45133  fourierdlem41  45162  fourierdlem42  45163  fourierdlem48  45168  fourierdlem49  45169  fourierdlem51  45171  fourierdlem73  45193  fourierdlem74  45194  fourierdlem75  45195  fourierdlem97  45217  etransclem24  45272  ioorrnopnlem  45318  issalnnd  45359  sge0rpcpnf  45435  sge0seq  45460  meaiuninc3v  45498  smfmullem4  45808  smflimsupmpt  45843  smfliminfmpt  45846  lincdifsn  47192