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  7736  caucvgprlemm  7752  caucvgprlemladdrl  7762  caucvgprlemlim  7765  caucvgprprlemml  7778  caucvgprprlemexbt  7790  caucvgprprlemlim  7795  suplocexprlemmu  7802  suplocexprlemloc  7805  suplocexprlemlub  7808  caucvgsrlemgt1  7879  suplocsrlemb  7890  suplocsrlem  7892  axcaucvglemres  7983  xaddval  9937  rebtwn2zlemstep  10359  nn0ltexp2  10818  hashunlem  10913  caucvgre  11163  cvg1nlemres  11167  resqrexlemglsq  11204  maxabslemval  11390  xrmaxiflemcl  11427  xrmaxifle  11428  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxiflemval  11432  xrmaxltsup  11440  divalglemeunn  12103  dvdsbnd  12148  bezoutlemnewy  12188  bezoutlemmain  12190  nninfctlemfo  12232  isprm5lem  12334  ctiunctlemfo  12681  prdsval  12975  sgrpidmndm  13122  mhmmnd  13322  mulgval  13328  txlm  14599  xmettx  14830  txmetcnp  14838  dedekindeu  14943  suplociccreex  14944  dedekindicclemlu  14950  dedekindicclemicc  14952  limcimo  14985  limccnp2cntop  14997  dvply2g  15086  lgsne0  15363