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  6624  tfrcllemaccex  6637  fimax2gtri  7212  en2eqpr  7220  unsnfidcex  7233  unsnfidcel  7234  fissfi  7269  ctssdc  7460  cauappcvgprlemloc  8026  caucvgprlemm  8042  caucvgprlemladdrl  8052  caucvgprlemlim  8055  caucvgprprlemml  8068  caucvgprprlemexbt  8080  caucvgprprlemlim  8085  suplocexprlemmu  8092  suplocexprlemloc  8095  suplocexprlemlub  8098  caucvgsrlemgt1  8169  suplocsrlemb  8180  suplocsrlem  8182  axcaucvglemres  8273  xaddval  10264  rebtwn2zlemstep  10704  nn0ltexp2  11169  hashunlem  11266  caucvgre  11769  cvg1nlemres  11773  resqrexlemglsq  11810  maxabslemval  11997  xrmaxiflemcl  12036  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemval  12041  xrmaxltsup  12049  divalglemeunn  12713  dvdsbnd  12758  bezoutlemnewy  12798  bezoutlemmain  12800  nninfctlemfo  12842  isprm5lem  12945  ctiunctlemfo  13388  sgrpidmndm  13792  mhmmnd  13978  mulgval  13984  gsumvalfi  14242  gsumzfi  14248  gsummptfidmsplit  14254  gsumresfi  14263  prdsval  14280  psrbaglefifi  15175  psrbaglefimap  15183  psrbagfsuppub  15192  mplsubrglemcl  15249  txlm  15538  xmettx  15769  txmetcnp  15777  dedekindeu  15882  suplociccreex  15883  dedekindicclemlu  15889  dedekindicclemicc  15891  limcimo  15924  limccnp2cntop  15936  dvply2g  16025  lgsne0  16395