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  6446  tfrcllemaccex  6459  fimax2gtri  7012  en2eqpr  7018  unsnfidcex  7031  unsnfidcel  7032  ctssdc  7229  cauappcvgprlemloc  7780  caucvgprlemm  7796  caucvgprlemladdrl  7806  caucvgprlemlim  7809  caucvgprprlemml  7822  caucvgprprlemexbt  7834  caucvgprprlemlim  7839  suplocexprlemmu  7846  suplocexprlemloc  7849  suplocexprlemlub  7852  caucvgsrlemgt1  7923  suplocsrlemb  7934  suplocsrlem  7936  axcaucvglemres  8027  xaddval  9982  rebtwn2zlemstep  10412  nn0ltexp2  10871  hashunlem  10966  caucvgre  11362  cvg1nlemres  11366  resqrexlemglsq  11403  maxabslemval  11589  xrmaxiflemcl  11626  xrmaxifle  11627  xrmaxiflemab  11628  xrmaxiflemlub  11629  xrmaxiflemval  11631  xrmaxltsup  11639  divalglemeunn  12302  dvdsbnd  12347  bezoutlemnewy  12387  bezoutlemmain  12389  nninfctlemfo  12431  isprm5lem  12533  ctiunctlemfo  12880  prdsval  13175  sgrpidmndm  13322  mhmmnd  13522  mulgval  13528  txlm  14821  xmettx  15052  txmetcnp  15060  dedekindeu  15165  suplociccreex  15166  dedekindicclemlu  15172  dedekindicclemicc  15174  limcimo  15207  limccnp2cntop  15219  dvply2g  15308  lgsne0  15585