Theorem ad4ant13 749

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 481	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 717	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad5ant14  756  ad5ant24  759  fntpb  7213  peano5  7886  peano5OLD  7887  f1o2ndf1  8110  cantnfle  9668  cantnflem1c  9684  ttukeylem5  10510  rlimsqzlem  15597  dvdslcmf  16570  poslubmo  18366  posglbmo  18367  smndex1mgm  18790  isgrpinv  18880  ghmgrp  18951  dprdfcntz  19887  sraassab  21428  cply1coe0bi  21831  isnrm3  22870  cnextcn  23578  ustexsym  23727  ustex2sym  23728  ustex3sym  23729  trust  23741  fmucnd  23804  trcfilu  23806  metust  24074  cxpmul2z  26206  umgrres1lem  28605  upgrres1  28608  friendshipgt3  29689  ccatf1  32153  cyc3evpm  32350  znfermltl  32524  rhmimaidl  32595  evls1fpws  32691  txomap  32883  zart0  32928  repr0  33692  breprexplemc  33713  hgt750lemb  33737  satffunlem1lem2  34463  satffunlem2lem2  34466  lindsadd  36567  matunitlindflem1  36570  nadd1suc  42224  mapss2  43983  supxrge  44127  xrlexaddrp  44141  infxr  44156  infleinf  44161  unb2ltle  44204  supminfxr  44253  limsuppnfdlem  44496  limsupub  44499  limsuppnflem  44505  climinf3  44511  limsupmnflem  44515  climxrre  44545  liminfvalxr  44578  fperdvper  44714  sge0isum  45222  sge0gtfsumgt  45238  sge0seq  45241  nnfoctbdjlem  45250  meaiuninc3v  45279  omeiunltfirp  45314  hspdifhsp  45411  hspmbllem2  45422  pimdecfgtioo  45512  pimincfltioo  45513  preimageiingt  45515  preimaleiinlt  45516  smfid  45547  proththd  46361  pzriprnglem4  46887