Theorem ad5antr 766

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 764	. 2 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
3	2	adantr 480	1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ad6antr  768  catass  16170  catpropd  16192  cidpropd  16193  monpropd  16220  funcpropd  16383  fucpropd  16460  drsdirfi  16761  mhmmnd  17360  neitr  20794  xkoccn  21232  trust  21843  restutopopn  21852  ucncn  21899  trcfilu  21908  ulmcau  23953  lgamucov  24564  tgcgrxfr  25213  tgbtwnconn1  25270  legov  25280  legso  25294  midexlem  25387  perpneq  25409  footex  25413  colperpexlem3  25424  colperpex  25425  opphllem  25427  opphllem3  25441  outpasch  25447  hlpasch  25448  lmieu  25476  trgcopy  25496  trgcopyeu  25498  dfcgra2  25521  acopyeu  25525  cgrg3col4  25534  f1otrg  25551  pthdepisspth  26104  omndmul2  29043  fimaproj  29228  qtophaus  29231  locfinreflem  29235  matunitlindflem1  32575  heicant  32614  mblfinlem3  32618  mblfinlem4  32619  itg2gt0cn  32635  sstotbnd2  32743  pell1234qrdich  36443  supxrgelem  38494  icccncfext  38773  etransclem35  39162  smflimlem2  39658