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  6500  tfrcllemaccex  6513  fimax2gtri  7071  en2eqpr  7077  unsnfidcex  7090  unsnfidcel  7091  ctssdc  7288  cauappcvgprlemloc  7847  caucvgprlemm  7863  caucvgprlemladdrl  7873  caucvgprlemlim  7876  caucvgprprlemml  7889  caucvgprprlemexbt  7901  caucvgprprlemlim  7906  suplocexprlemmu  7913  suplocexprlemloc  7916  suplocexprlemlub  7919  caucvgsrlemgt1  7990  suplocsrlemb  8001  suplocsrlem  8003  axcaucvglemres  8094  xaddval  10049  rebtwn2zlemstep  10480  nn0ltexp2  10939  hashunlem  11034  caucvgre  11500  cvg1nlemres  11504  resqrexlemglsq  11541  maxabslemval  11727  xrmaxiflemcl  11764  xrmaxifle  11765  xrmaxiflemab  11766  xrmaxiflemlub  11767  xrmaxiflemval  11769  xrmaxltsup  11777  divalglemeunn  12440  dvdsbnd  12485  bezoutlemnewy  12525  bezoutlemmain  12527  nninfctlemfo  12569  isprm5lem  12671  ctiunctlemfo  13018  prdsval  13314  sgrpidmndm  13461  mhmmnd  13661  mulgval  13667  txlm  14961  xmettx  15192  txmetcnp  15200  dedekindeu  15305  suplociccreex  15306  dedekindicclemlu  15312  dedekindicclemicc  15314  limcimo  15347  limccnp2cntop  15359  dvply2g  15448  lgsne0  15725