Theorem ad6antr 737

Description: Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad6antr	⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)

Proof of Theorem ad6antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad5antr 735	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:  ad7antr  739  ad7antlr  740  simp-6l  787  catass  17643  funcpropd  17860  natpropd  17937  ghmqusnsg  19248  ghmquskerlem3  19252  rhmqusnsg  21275  restutop  24212  utopreg  24227  restmetu  24545  lgamucov  27015  istrkgcb  28538  tgifscgr  28590  tgbtwnconn1lem3  28656  legtrd  28671  miriso  28752  footexALT  28800  footex  28803  opphllem3  28831  opphl  28836  trgcopy  28886  cgratr  28905  dfcgra2  28912  inaghl  28927  cgrg3col4  28935  f1otrge  28954  clwlkclwwlklem2  30085  gsumwun  33152  cyc3genpm  33228  elrgspnlem4  33321  erler  33341  rlocaddval  33344  rlocmulval  33345  rloccring  33346  rhmquskerlem  33500  elrspunidl  33503  rhmimaidl  33507  ssdifidllem  33531  ssdifidlprm  33533  mxidlirredi  33546  mxidlirred  33547  ssmxidllem  33548  qsdrngi  33570  1arithidom  33612  1arithufdlem3  33621  r1plmhm  33685  r1pquslmic  33686  lbsdiflsp0  33786  dimkerim  33787  fedgmul  33791  fldextrspunlsplem  33833  fldext2chn  33888  constrextdg2lem  33908  txomap  33994  matunitlindflem1  37951  heicant  37990  mblfinlem3  37994  primrootscoprmpow  42552  aks6d1c2lem4  42580  aks6d1c5  42592  limclner  46097  hoidmvle  47046  chnerlem1  47328