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  10197  rebtwn2zlemstep  10636  nn0ltexp2  11096  hashunlem  11193  caucvgre  11691  cvg1nlemres  11695  resqrexlemglsq  11732  maxabslemval  11918  xrmaxiflemcl  11955  xrmaxifle  11956  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxiflemval  11960  xrmaxltsup  11968  divalglemeunn  12632  dvdsbnd  12677  bezoutlemnewy  12717  bezoutlemmain  12719  nninfctlemfo  12761  isprm5lem  12863  ctiunctlemfo  13274  prdsval  13570  sgrpidmndm  13717  mhmmnd  13917  mulgval  13923  txlm  15256  xmettx  15487  txmetcnp  15495  dedekindeu  15600  suplociccreex  15601  dedekindicclemlu  15607  dedekindicclemicc  15609  limcimo  15642  limccnp2cntop  15654  dvply2g  15743  lgsne0  16023  gfsumval  16974  gfsumz  16981