Theorem ad5antr 765

Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem ad5antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad4antr 763	. 2 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
3	2	adantr 479	1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  ad6antr  767  catass  16118  catpropd  16140  cidpropd  16141  monpropd  16168  funcpropd  16331  fucpropd  16408  drsdirfi  16709  mhmmnd  17308  neitr  20741  xkoccn  21179  trust  21790  restutopopn  21799  ucncn  21846  trcfilu  21855  ulmcau  23897  lgamucov  24508  tgcgrxfr  25158  tgbtwnconn1  25215  legov  25225  legso  25239  midexlem  25332  perpneq  25354  footex  25358  colperpexlem3  25369  colperpex  25370  opphllem  25372  opphllem3  25386  outpasch  25392  hlpasch  25393  lmieu  25421  trgcopy  25441  trgcopyeu  25443  dfcgra2  25466  acopyeu  25470  cgrg3col4  25479  f1otrg  25496  pthdepisspth  25897  omndmul2  28836  fimaproj  29021  qtophaus  29024  locfinreflem  29028  matunitlindflem1  32358  heicant  32397  mblfinlem3  32401  mblfinlem4  32402  itg2gt0cn  32418  sstotbnd2  32526  pell1234qrdich  36226  supxrgelem  38277  icccncfext  38556  etransclem35  38945  smflimlem2  39441