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:  dif1enALT  8980  infpssrlem4  9993  fin23lem11  10004  tskwun  10471  gruf  10498  lediv2a  11799  prunioo  13142  nn0p1elfzo  13358  hashunsnggt  14037  rpnnen2lem7  15857  muldvds1  15918  muldvds2  15919  dvdscmul  15920  dvdsmulc  15921  rpexp  16355  pospropd  17960  mdetmul  21680  elcls  22132  iscnp4  22322  cnpnei  22323  cnpflf2  23059  cnpflf  23060  cnpfcf  23100  xbln0  23475  blcls  23568  iimulcl  24006  icccvx  24019  iscau2  24346  rrxcph  24461  cncombf  24727  mumul  26235  ax5seglem1  27199  ax5seglem2  27200  wwlksnext  28159  clwwlkinwwlk  28305  nvmul0or  28913  fh1  29881  fh2  29882  cm2j  29883  pjoi0  29980  hoadddi  30066  hmopco  30286  padct  30956  iocinif  31004  volfiniune  32098  eulerpartlemb  32235  noetalem1  33871  ivthALT  34451  lindsadd  35697  cnambfre  35752  rngohomco  36059  rngoisoco  36067  pexmidlem3N  37913  hdmapglem7  39870  sticksstones12a  40041  factwoffsmonot  40091  relexpmulg  41207  supxrgere  42762  supxrgelem  42766  supxrge  42767  infxr  42796  infleinflem2  42800  rexabslelem  42848  lptre2pt  43071  fnlimfvre  43105  limsupmnfuzlem  43157  climisp  43177  limsupgtlem  43208  dvnprodlem1  43377  ibliccsinexp  43382  iblioosinexp  43384  fourierdlem12  43550  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem97  43634  etransclem24  43689  ioorrnopnlem  43735  issalnnd  43774  sge0rpcpnf  43849  sge0seq  43874  meaiuninc3v  43912  smfmullem4  44215  smflimsupmpt  44249  smfliminfmpt  44252  lincdifsn  45653