Theorem ad4antr 494

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

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem ad4antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad3antrrr 492	. 2 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
3	2	adantr 276	1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad5antr  496  tfr1onlemaccex  6592  tfrcllemaccex  6605  fimax2gtri  7172  en2eqpr  7180  unsnfidcex  7193  unsnfidcel  7194  fissfi  7229  ctssdc  7417  cauappcvgprlemloc  7983  caucvgprlemm  7999  caucvgprlemladdrl  8009  caucvgprlemlim  8012  caucvgprprlemml  8025  caucvgprprlemexbt  8037  caucvgprprlemlim  8042  suplocexprlemmu  8049  suplocexprlemloc  8052  suplocexprlemlub  8055  caucvgsrlemgt1  8126  suplocsrlemb  8137  suplocsrlem  8139  axcaucvglemres  8230  xaddval  10200  rebtwn2zlemstep  10639  nn0ltexp2  11099  hashunlem  11196  caucvgre  11695  cvg1nlemres  11699  resqrexlemglsq  11736  maxabslemval  11922  xrmaxiflemcl  11959  xrmaxifle  11960  xrmaxiflemab  11961  xrmaxiflemlub  11962  xrmaxiflemval  11964  xrmaxltsup  11972  divalglemeunn  12636  dvdsbnd  12681  bezoutlemnewy  12721  bezoutlemmain  12723  nninfctlemfo  12765  isprm5lem  12867  ctiunctlemfo  13278  sgrpidmndm  13685  mhmmnd  13873  mulgval  13879  gfsumval  14106  gfsumz  14113  prdsval  14119  txlm  15274  xmettx  15505  txmetcnp  15513  dedekindeu  15618  suplociccreex  15619  dedekindicclemlu  15625  dedekindicclemicc  15627  limcimo  15660  limccnp2cntop  15672  dvply2g  15761  lgsne0  16041