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  6623  tfrcllemaccex  6636  fimax2gtri  7211  en2eqpr  7219  unsnfidcex  7232  unsnfidcel  7233  fissfi  7268  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  10265  rebtwn2zlemstep  10705  nn0ltexp2  11170  hashunlem  11267  caucvgre  11770  cvg1nlemres  11774  resqrexlemglsq  11811  maxabslemval  11998  xrmaxiflemcl  12037  xrmaxifle  12038  xrmaxiflemab  12039  xrmaxiflemlub  12040  xrmaxiflemval  12042  xrmaxltsup  12050  divalglemeunn  12714  dvdsbnd  12759  bezoutlemnewy  12799  bezoutlemmain  12801  nninfctlemfo  12843  isprm5lem  12946  ctiunctlemfo  13389  sgrpidmndm  13793  mhmmnd  13979  mulgval  13985  gsumvalfi  14243  gsumzfi  14249  gsummptfidmsplit  14255  gsumresfi  14264  prdsval  14281  psrbaglefifi  15177  txlm  15517  xmettx  15748  txmetcnp  15756  dedekindeu  15861  suplociccreex  15862  dedekindicclemlu  15868  dedekindicclemicc  15870  limcimo  15903  limccnp2cntop  15915  dvply2g  16004  lgsne0  16374