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  6505  tfrcllemaccex  6518  fimax2gtri  7077  en2eqpr  7085  unsnfidcex  7098  unsnfidcel  7099  ctssdc  7296  cauappcvgprlemloc  7855  caucvgprlemm  7871  caucvgprlemladdrl  7881  caucvgprlemlim  7884  caucvgprprlemml  7897  caucvgprprlemexbt  7909  caucvgprprlemlim  7914  suplocexprlemmu  7921  suplocexprlemloc  7924  suplocexprlemlub  7927  caucvgsrlemgt1  7998  suplocsrlemb  8009  suplocsrlem  8011  axcaucvglemres  8102  xaddval  10058  rebtwn2zlemstep  10489  nn0ltexp2  10948  hashunlem  11043  caucvgre  11513  cvg1nlemres  11517  resqrexlemglsq  11554  maxabslemval  11740  xrmaxiflemcl  11777  xrmaxifle  11778  xrmaxiflemab  11779  xrmaxiflemlub  11780  xrmaxiflemval  11782  xrmaxltsup  11790  divalglemeunn  12453  dvdsbnd  12498  bezoutlemnewy  12538  bezoutlemmain  12540  nninfctlemfo  12582  isprm5lem  12684  ctiunctlemfo  13031  prdsval  13327  sgrpidmndm  13474  mhmmnd  13674  mulgval  13680  txlm  14974  xmettx  15205  txmetcnp  15213  dedekindeu  15318  suplociccreex  15319  dedekindicclemlu  15325  dedekindicclemicc  15327  limcimo  15360  limccnp2cntop  15372  dvply2g  15461  lgsne0  15738