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  6514  tfrcllemaccex  6527  fimax2gtri  7091  en2eqpr  7099  unsnfidcex  7112  unsnfidcel  7113  ctssdc  7312  cauappcvgprlemloc  7872  caucvgprlemm  7888  caucvgprlemladdrl  7898  caucvgprlemlim  7901  caucvgprprlemml  7914  caucvgprprlemexbt  7926  caucvgprprlemlim  7931  suplocexprlemmu  7938  suplocexprlemloc  7941  suplocexprlemlub  7944  caucvgsrlemgt1  8015  suplocsrlemb  8026  suplocsrlem  8028  axcaucvglemres  8119  xaddval  10080  rebtwn2zlemstep  10513  nn0ltexp2  10972  hashunlem  11068  caucvgre  11546  cvg1nlemres  11550  resqrexlemglsq  11587  maxabslemval  11773  xrmaxiflemcl  11810  xrmaxifle  11811  xrmaxiflemab  11812  xrmaxiflemlub  11813  xrmaxiflemval  11815  xrmaxltsup  11823  divalglemeunn  12487  dvdsbnd  12532  bezoutlemnewy  12572  bezoutlemmain  12574  nninfctlemfo  12616  isprm5lem  12718  ctiunctlemfo  13065  prdsval  13361  sgrpidmndm  13508  mhmmnd  13708  mulgval  13714  txlm  15009  xmettx  15240  txmetcnp  15248  dedekindeu  15353  suplociccreex  15354  dedekindicclemlu  15360  dedekindicclemicc  15362  limcimo  15395  limccnp2cntop  15407  dvply2g  15496  lgsne0  15773  gfsumval  16706