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 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

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  500  tfr1onlemaccex  6613  tfrcllemaccex  6626  fimax2gtri  7200  en2eqpr  7208  unsnfidcex  7221  unsnfidcel  7222  fissfi  7257  ctssdc  7447  cauappcvgprlemloc  8013  caucvgprlemm  8029  caucvgprlemladdrl  8039  caucvgprlemlim  8042  caucvgprprlemml  8055  caucvgprprlemexbt  8067  caucvgprprlemlim  8072  suplocexprlemmu  8079  suplocexprlemloc  8082  suplocexprlemlub  8085  caucvgsrlemgt1  8156  suplocsrlemb  8167  suplocsrlem  8169  axcaucvglemres  8260  xaddval  10230  rebtwn2zlemstep  10670  nn0ltexp2  11130  hashunlem  11227  caucvgre  11730  cvg1nlemres  11734  resqrexlemglsq  11771  maxabslemval  11957  xrmaxiflemcl  11994  xrmaxifle  11995  xrmaxiflemab  11996  xrmaxiflemlub  11997  xrmaxiflemval  11999  xrmaxltsup  12007  divalglemeunn  12671  dvdsbnd  12716  bezoutlemnewy  12756  bezoutlemmain  12758  nninfctlemfo  12800  isprm5lem  12902  ctiunctlemfo  13313  sgrpidmndm  13716  mhmmnd  13902  mulgval  13908  gsumvalfi  14135  gsumzfi  14141  prdsval  14156  txlm  15363  xmettx  15594  txmetcnp  15602  dedekindeu  15707  suplociccreex  15708  dedekindicclemlu  15714  dedekindicclemicc  15716  limcimo  15749  limccnp2cntop  15761  dvply2g  15850  lgsne0  16140