Theorem 3adantl3 1169

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 1149	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜏) → (𝜑 ∧ 𝜓))
2		3adantl.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylan 580	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

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

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 1089

This theorem is referenced by:  dif1ennnALT  9311  infpssrlem4  10346  fin23lem11  10357  tskwun  10824  gruf  10851  lediv2a  12162  prunioo  13521  nn0p1elfzo  13742  hashunsnggt  14433  rpnnen2lem7  16256  muldvds1  16318  muldvds2  16319  dvdscmul  16320  dvdsmulc  16321  rpexp  16759  pospropd  18372  mdetmul  22629  elcls  23081  iscnp4  23271  cnpnei  23272  cnpflf2  24008  cnpflf  24009  cnpfcf  24049  xbln0  24424  blcls  24519  iimulcl  24966  icccvx  24981  iscau2  25311  rrxcph  25426  cncombf  25693  mumul  27224  noetalem1  27786  ax5seglem1  28943  ax5seglem2  28944  wwlksnext  29913  clwwlkinwwlk  30059  nvmul0or  30669  fh1  31637  fh2  31638  cm2j  31639  pjoi0  31736  hoadddi  31822  hmopco  32042  padct  32731  iocinif  32783  volfiniune  34231  eulerpartlemb  34370  ivthALT  36336  lindsadd  37620  cnambfre  37675  rngohomco  37981  rngoisoco  37989  pexmidlem3N  39974  hdmapglem7  41931  sticksstones12a  42158  factwoffsmonot  42243  relexpmulg  43723  supxrgere  45344  supxrgelem  45348  supxrge  45349  infxr  45378  infleinflem2  45382  rexabslelem  45429  pimxrneun  45499  lptre2pt  45655  fnlimfvre  45689  limsupmnfuzlem  45741  climisp  45761  limsupgtlem  45792  dvnprodlem1  45961  ibliccsinexp  45966  iblioosinexp  45968  fourierdlem12  46134  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem97  46218  etransclem24  46273  ioorrnopnlem  46319  issalnnd  46360  sge0rpcpnf  46436  sge0seq  46461  meaiuninc3v  46499  smfmullem4  46809  smflimsupmpt  46844  smfliminfmpt  46847  lincdifsn  48341