Theorem ad5antr 770

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  ad6antr  772  catass  16347  catpropd  16369  cidpropd  16370  monpropd  16397  funcpropd  16560  fucpropd  16637  drsdirfi  16938  mhmmnd  17537  neitr  20984  xkoccn  21422  trust  22033  restutopopn  22042  ucncn  22089  trcfilu  22098  ulmcau  24149  lgamucov  24764  tgcgrxfr  25413  tgbtwnconn1  25470  legov  25480  legso  25494  midexlem  25587  perpneq  25609  footex  25613  colperpexlem3  25624  colperpex  25625  opphllem  25627  opphllem3  25641  outpasch  25647  hlpasch  25648  lmieu  25676  trgcopy  25696  trgcopyeu  25698  dfcgra2  25721  acopyeu  25725  cgrg3col4  25734  f1otrg  25751  omndmul2  29712  fimaproj  29900  qtophaus  29903  locfinreflem  29907  hgt750lemb  30734  matunitlindflem1  33405  heicant  33444  mblfinlem3  33448  mblfinlem4  33449  itg2gt0cn  33465  sstotbnd2  33573  pell1234qrdich  37425  supxrgelem  39553  icccncfext  40100  etransclem35  40486  smflimlem2  40980