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  6351  tfrcllemaccex  6364  fimax2gtri  6903  en2eqpr  6909  unsnfidcex  6921  unsnfidcel  6922  ctssdc  7114  cauappcvgprlemloc  7653  caucvgprlemm  7669  caucvgprlemladdrl  7679  caucvgprlemlim  7682  caucvgprprlemml  7695  caucvgprprlemexbt  7707  caucvgprprlemlim  7712  suplocexprlemmu  7719  suplocexprlemloc  7722  suplocexprlemlub  7725  caucvgsrlemgt1  7796  suplocsrlemb  7807  suplocsrlem  7809  axcaucvglemres  7900  xaddval  9847  rebtwn2zlemstep  10255  nn0ltexp2  10691  hashunlem  10786  caucvgre  10992  cvg1nlemres  10996  resqrexlemglsq  11033  maxabslemval  11219  xrmaxiflemcl  11255  xrmaxifle  11256  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxiflemval  11260  xrmaxltsup  11268  divalglemeunn  11928  dvdsbnd  11959  bezoutlemnewy  11999  bezoutlemmain  12001  isprm5lem  12143  ctiunctlemfo  12442  sgrpidmndm  12826  mhmmnd  12985  mulgval  12991  txlm  13818  xmettx  14049  txmetcnp  14057  dedekindeu  14140  suplociccreex  14141  dedekindicclemlu  14147  dedekindicclemicc  14149  limcimo  14173  limccnp2cntop  14185  lgsne0  14478