Theorem ad4antr 498

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 496	. 2 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
3	2	adantr 276	1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad5antr  500  tfr1onlemaccex  6619  tfrcllemaccex  6632  fimax2gtri  7206  en2eqpr  7214  unsnfidcex  7227  unsnfidcel  7228  fissfi  7263  ctssdc  7453  cauappcvgprlemloc  8019  caucvgprlemm  8035  caucvgprlemladdrl  8045  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemexbt  8073  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemloc  8088  suplocexprlemlub  8091  caucvgsrlemgt1  8162  suplocsrlemb  8173  suplocsrlem  8175  axcaucvglemres  8266  xaddval  10249  rebtwn2zlemstep  10689  nn0ltexp2  11149  hashunlem  11246  caucvgre  11749  cvg1nlemres  11753  resqrexlemglsq  11790  maxabslemval  11976  xrmaxiflemcl  12013  xrmaxifle  12014  xrmaxiflemab  12015  xrmaxiflemlub  12016  xrmaxiflemval  12018  xrmaxltsup  12026  divalglemeunn  12690  dvdsbnd  12735  bezoutlemnewy  12775  bezoutlemmain  12777  nninfctlemfo  12819  isprm5lem  12921  ctiunctlemfo  13332  sgrpidmndm  13735  mhmmnd  13921  mulgval  13927  gsumvalfi  14154  gsumzfi  14160  prdsval  14175  txlm  15382  xmettx  15613  txmetcnp  15621  dedekindeu  15726  suplociccreex  15727  dedekindicclemlu  15733  dedekindicclemicc  15735  limcimo  15768  limccnp2cntop  15780  dvply2g  15869  lgsne0  16169