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  6509  tfrcllemaccex  6522  fimax2gtri  7086  en2eqpr  7094  unsnfidcex  7107  unsnfidcel  7108  ctssdc  7306  cauappcvgprlemloc  7865  caucvgprlemm  7881  caucvgprlemladdrl  7891  caucvgprlemlim  7894  caucvgprprlemml  7907  caucvgprprlemexbt  7919  caucvgprprlemlim  7924  suplocexprlemmu  7931  suplocexprlemloc  7934  suplocexprlemlub  7937  caucvgsrlemgt1  8008  suplocsrlemb  8019  suplocsrlem  8021  axcaucvglemres  8112  xaddval  10073  rebtwn2zlemstep  10505  nn0ltexp2  10964  hashunlem  11060  caucvgre  11535  cvg1nlemres  11539  resqrexlemglsq  11576  maxabslemval  11762  xrmaxiflemcl  11799  xrmaxifle  11800  xrmaxiflemab  11801  xrmaxiflemlub  11802  xrmaxiflemval  11804  xrmaxltsup  11812  divalglemeunn  12475  dvdsbnd  12520  bezoutlemnewy  12560  bezoutlemmain  12562  nninfctlemfo  12604  isprm5lem  12706  ctiunctlemfo  13053  prdsval  13349  sgrpidmndm  13496  mhmmnd  13696  mulgval  13702  txlm  14996  xmettx  15227  txmetcnp  15235  dedekindeu  15340  suplociccreex  15341  dedekindicclemlu  15347  dedekindicclemicc  15349  limcimo  15382  limccnp2cntop  15394  dvply2g  15483  lgsne0  15760  gfsumval  16630