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  6415  tfrcllemaccex  6428  fimax2gtri  6971  en2eqpr  6977  unsnfidcex  6990  unsnfidcel  6991  ctssdc  7188  cauappcvgprlemloc  7738  caucvgprlemm  7754  caucvgprlemladdrl  7764  caucvgprlemlim  7767  caucvgprprlemml  7780  caucvgprprlemexbt  7792  caucvgprprlemlim  7797  suplocexprlemmu  7804  suplocexprlemloc  7807  suplocexprlemlub  7810  caucvgsrlemgt1  7881  suplocsrlemb  7892  suplocsrlem  7894  axcaucvglemres  7985  xaddval  9939  rebtwn2zlemstep  10361  nn0ltexp2  10820  hashunlem  10915  caucvgre  11165  cvg1nlemres  11169  resqrexlemglsq  11206  maxabslemval  11392  xrmaxiflemcl  11429  xrmaxifle  11430  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxiflemval  11434  xrmaxltsup  11442  divalglemeunn  12105  dvdsbnd  12150  bezoutlemnewy  12190  bezoutlemmain  12192  nninfctlemfo  12234  isprm5lem  12336  ctiunctlemfo  12683  prdsval  12977  sgrpidmndm  13124  mhmmnd  13324  mulgval  13330  txlm  14623  xmettx  14854  txmetcnp  14862  dedekindeu  14967  suplociccreex  14968  dedekindicclemlu  14974  dedekindicclemicc  14976  limcimo  15009  limccnp2cntop  15021  dvply2g  15110  lgsne0  15387