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  6339  tfrcllemaccex  6352  fimax2gtri  6891  en2eqpr  6897  unsnfidcex  6909  unsnfidcel  6910  ctssdc  7102  cauappcvgprlemloc  7626  caucvgprlemm  7642  caucvgprlemladdrl  7652  caucvgprlemlim  7655  caucvgprprlemml  7668  caucvgprprlemexbt  7680  caucvgprprlemlim  7685  suplocexprlemmu  7692  suplocexprlemloc  7695  suplocexprlemlub  7698  caucvgsrlemgt1  7769  suplocsrlemb  7780  suplocsrlem  7782  axcaucvglemres  7873  xaddval  9814  rebtwn2zlemstep  10221  nn0ltexp2  10656  hashunlem  10750  caucvgre  10956  cvg1nlemres  10960  resqrexlemglsq  10997  maxabslemval  11183  xrmaxiflemcl  11219  xrmaxifle  11220  xrmaxiflemab  11221  xrmaxiflemlub  11222  xrmaxiflemval  11224  xrmaxltsup  11232  divalglemeunn  11891  dvdsbnd  11922  bezoutlemnewy  11962  bezoutlemmain  11964  isprm5lem  12106  ctiunctlemfo  12405  sgrpidmndm  12685  mhmmnd  12839  mulgval  12845  txlm  13330  xmettx  13561  txmetcnp  13569  dedekindeu  13652  suplociccreex  13653  dedekindicclemlu  13659  dedekindicclemicc  13661  limcimo  13685  limccnp2cntop  13697  lgsne0  13990