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  6557  tfrcllemaccex  6570  fimax2gtri  7134  en2eqpr  7142  unsnfidcex  7155  unsnfidcel  7156  ctssdc  7355  cauappcvgprlemloc  7915  caucvgprlemm  7931  caucvgprlemladdrl  7941  caucvgprlemlim  7944  caucvgprprlemml  7957  caucvgprprlemexbt  7969  caucvgprprlemlim  7974  suplocexprlemmu  7981  suplocexprlemloc  7984  suplocexprlemlub  7987  caucvgsrlemgt1  8058  suplocsrlemb  8069  suplocsrlem  8071  axcaucvglemres  8162  xaddval  10123  rebtwn2zlemstep  10556  nn0ltexp2  11015  hashunlem  11111  caucvgre  11602  cvg1nlemres  11606  resqrexlemglsq  11643  maxabslemval  11829  xrmaxiflemcl  11866  xrmaxifle  11867  xrmaxiflemab  11868  xrmaxiflemlub  11869  xrmaxiflemval  11871  xrmaxltsup  11879  divalglemeunn  12543  dvdsbnd  12588  bezoutlemnewy  12628  bezoutlemmain  12630  nninfctlemfo  12672  isprm5lem  12774  ctiunctlemfo  13121  prdsval  13417  sgrpidmndm  13564  mhmmnd  13764  mulgval  13770  txlm  15070  xmettx  15301  txmetcnp  15309  dedekindeu  15414  suplociccreex  15415  dedekindicclemlu  15421  dedekindicclemicc  15423  limcimo  15456  limccnp2cntop  15468  dvply2g  15557  lgsne0  15837  gfsumval  16789