Theorem ad4antr 498

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 496	. 2 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
3	2	adantr 276	1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad5antr  500  tfr1onlemaccex  6619  tfrcllemaccex  6632  fimax2gtri  7206  en2eqpr  7214  unsnfidcex  7227  unsnfidcel  7228  fissfi  7263  ctssdc  7454  cauappcvgprlemloc  8020  caucvgprlemm  8036  caucvgprlemladdrl  8046  caucvgprlemlim  8049  caucvgprprlemml  8062  caucvgprprlemexbt  8074  caucvgprprlemlim  8079  suplocexprlemmu  8086  suplocexprlemloc  8089  suplocexprlemlub  8092  caucvgsrlemgt1  8163  suplocsrlemb  8174  suplocsrlem  8176  axcaucvglemres  8267  xaddval  10258  rebtwn2zlemstep  10698  nn0ltexp2  11162  hashunlem  11259  caucvgre  11762  cvg1nlemres  11766  resqrexlemglsq  11803  maxabslemval  11990  xrmaxiflemcl  12029  xrmaxifle  12030  xrmaxiflemab  12031  xrmaxiflemlub  12032  xrmaxiflemval  12034  xrmaxltsup  12042  divalglemeunn  12706  dvdsbnd  12751  bezoutlemnewy  12791  bezoutlemmain  12793  nninfctlemfo  12835  isprm5lem  12938  ctiunctlemfo  13381  sgrpidmndm  13784  mhmmnd  13970  mulgval  13976  gsumvalfi  14203  gsumzfi  14209  prdsval  14224  psrbaglefifi  15114  txlm  15432  xmettx  15663  txmetcnp  15671  dedekindeu  15776  suplociccreex  15777  dedekindicclemlu  15783  dedekindicclemicc  15785  limcimo  15818  limccnp2cntop  15830  dvply2g  15919  lgsne0  16279