Theorem ad5antr 734

Description: Deduction adding 5 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
ad5antr	⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem ad5antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad4antr 732	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:  ad6antr  736  ad6antlr  737  simp-5l  784  fimaproj  8075  catass  17610  catpropd  17633  cidpropd  17634  monpropd  17662  funcpropd  17827  fucpropd  17905  drsdirfi  18229  mhmmnd  18961  ghmqusnsg  19179  ghmquskerlem3  19183  omndmul2  20030  rhmqusnsg  21210  neitr  23083  xkoccn  23522  trust  24133  restutopopn  24142  ucncn  24188  trcfilu  24197  ulmcau  26320  lgamucov  26964  tgcgrxfr  28481  tgbtwnconn1  28538  legov  28548  legso  28562  midexlem  28655  perpneq  28677  footexALT  28681  footex  28684  colperpexlem3  28695  colperpex  28696  opphllem  28698  opphllem3  28712  outpasch  28718  hlpasch  28719  lmieu  28747  trgcopy  28767  trgcopyeu  28769  dfcgra2  28793  acopyeu  28797  cgrg3col4  28816  f1otrg  28834  fnpreimac  32628  nn0xmulclb  32727  s3f1  32901  ccatws1f1o  32906  chnind  32966  mndlactf1o  32997  gsumwun  33031  gsumwrd2dccatlem  33032  cyc3conja  33112  elrgspnlem4  33195  erler  33215  rlocf1  33223  isdrng4  33244  fracfld  33257  dvdsruasso  33332  nsgqusf1olem3  33362  rhmquskerlem  33372  elrspunsn  33376  rhmimaidl  33379  ssdifidllem  33403  ssdifidlprm  33405  mxidlprm  33417  ssmxidllem  33420  qsdrng  33444  rprmasso2  33473  1arithufdlem3  33493  1arithufdlem4  33494  dfufd2lem  33496  fedgmul  33603  extdg1id  33637  constrextdg2lem  33714  qtophaus  33802  locfinreflem  33806  zarclssn  33839  hgt750lemb  34623  matunitlindflem1  37595  heicant  37634  mblfinlem3  37638  mblfinlem4  37639  itg2gt0cn  37654  sstotbnd2  37753  aks4d1p8  42060  aks6d1c2p2  42092  aks6d1c2  42103  aks6d1c6lem3  42145  unitscyglem3  42170  fsuppind  42563  pell1234qrdich  42834  omabs2  43305  supxrgelem  45317  icccncfext  45869  etransclem35  46251  smflimlem2  46754  uppropd  49167  fuco21  49322