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

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

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 1088

This theorem is referenced by:  dif1ennnALT  9177  infpssrlem4  10216  fin23lem11  10227  tskwun  10695  gruf  10722  lediv2a  12036  prunioo  13397  nn0p1elfzo  13618  hashunsnggt  14317  rpnnen2lem7  16145  muldvds1  16207  muldvds2  16208  dvdscmul  16209  dvdsmulc  16210  rpexp  16649  pospropd  18248  mdetmul  22567  elcls  23017  iscnp4  23207  cnpnei  23208  cnpflf2  23944  cnpflf  23945  cnpfcf  23985  xbln0  24358  blcls  24450  iimulcl  24889  icccvx  24904  iscau2  25233  rrxcph  25348  cncombf  25615  mumul  27147  noetalem1  27709  ax5seglem1  29001  ax5seglem2  29002  wwlksnext  29966  clwwlkinwwlk  30115  nvmul0or  30725  fh1  31693  fh2  31694  cm2j  31695  pjoi0  31792  hoadddi  31878  hmopco  32098  padct  32797  iocinif  32861  volfiniune  34387  eulerpartlemb  34525  ivthALT  36529  lindsadd  37814  cnambfre  37869  rngohomco  38175  rngoisoco  38183  pexmidlem3N  40232  hdmapglem7  42189  sticksstones12a  42411  relexpmulg  43951  supxrgere  45578  supxrgelem  45582  supxrge  45583  infxr  45611  infleinflem2  45615  rexabslelem  45662  pimxrneun  45732  lptre2pt  45884  fnlimfvre  45918  limsupmnfuzlem  45970  climisp  45990  limsupgtlem  46021  dvnprodlem1  46190  ibliccsinexp  46195  iblioosinexp  46197  fourierdlem12  46363  fourierdlem41  46392  fourierdlem42  46393  fourierdlem48  46398  fourierdlem49  46399  fourierdlem51  46401  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem97  46447  etransclem24  46502  ioorrnopnlem  46548  issalnnd  46589  sge0rpcpnf  46665  sge0seq  46690  meaiuninc3v  46728  smfmullem4  47038  smflimsupmpt  47073  smfliminfmpt  47076  lincdifsn  48670  uptrlem1  49455