Theorem ad4antr 485

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad5antr  487  tfr1onlemaccex  6238  tfrcllemaccex  6251  fimax2gtri  6788  en2eqpr  6794  unsnfidcex  6801  unsnfidcel  6802  ctssdc  6991  cauappcvgprlemloc  7453  caucvgprlemm  7469  caucvgprlemladdrl  7479  caucvgprlemlim  7482  caucvgprprlemml  7495  caucvgprprlemexbt  7507  caucvgprprlemlim  7512  suplocexprlemmu  7519  suplocexprlemloc  7522  suplocexprlemlub  7525  caucvgsrlemgt1  7596  suplocsrlemb  7607  suplocsrlem  7609  axcaucvglemres  7700  xaddval  9621  rebtwn2zlemstep  10023  hashunlem  10543  caucvgre  10746  cvg1nlemres  10750  resqrexlemglsq  10787  maxabslemval  10973  xrmaxiflemcl  11007  xrmaxifle  11008  xrmaxiflemab  11009  xrmaxiflemlub  11010  xrmaxiflemval  11012  xrmaxltsup  11020  divalglemeunn  11607  dvdsbnd  11634  bezoutlemnewy  11673  bezoutlemmain  11675  ctiunctlemfo  11941  txlm  12437  xmettx  12668  txmetcnp  12676  dedekindeu  12759  suplociccreex  12760  dedekindicclemlu  12766  dedekindicclemicc  12768  limcimo  12792  limccnp2cntop  12804