Theorem ad4ant13 751

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

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

Proof of Theorem ad4ant13

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantr 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 719	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  ad5ant14  757  ad5ant24  760  fntpb  7143  peano5  7823  f1o2ndf1  8052  cantnfle  9561  cantnflem1c  9577  ttukeylem5  10404  rlimsqzlem  15556  dvdslcmf  16542  poslubmo  18315  posglbmo  18316  smndex1mgm  18815  isgrpinv  18906  ghmgrp  18979  dprdfcntz  19929  pzriprnglem4  21421  sraassab  21805  cply1coe0bi  22217  evls1fpws  22284  isnrm3  23274  cnextcn  23982  ustexsym  24131  ustex2sym  24132  ustex3sym  24133  trust  24144  fmucnd  24206  trcfilu  24208  metust  24473  cxpmul2z  26627  umgrres1lem  29288  upgrres1  29291  friendshipgt3  30378  ccatf1  32930  cyc3evpm  33119  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  znfermltl  33331  rhmimaidl  33397  dimlssid  33645  txomap  33847  zart0  33892  repr0  34624  breprexplemc  34645  hgt750lemb  34669  satffunlem1lem2  35447  satffunlem2lem2  35450  lindsadd  37661  matunitlindflem1  37664  nadd1suc  43433  mapss2  45250  supxrge  45385  xrlexaddrp  45399  infxr  45413  infleinf  45418  unb2ltle  45461  supminfxr  45510  limsuppnfdlem  45747  limsupub  45750  limsuppnflem  45756  climinf3  45762  limsupmnflem  45766  climxrre  45796  liminfvalxr  45829  fperdvper  45965  sge0isum  46473  sge0gtfsumgt  46489  sge0seq  46492  nnfoctbdjlem  46501  meaiuninc3v  46530  omeiunltfirp  46565  hspdifhsp  46662  hspmbllem2  46673  pimdecfgtioo  46763  pimincfltioo  46764  preimageiingt  46766  preimaleiinlt  46767  smfid  46798  proththd  47653