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  6484  tfrcllemaccex  6497  fimax2gtri  7051  en2eqpr  7057  unsnfidcex  7070  unsnfidcel  7071  ctssdc  7268  cauappcvgprlemloc  7827  caucvgprlemm  7843  caucvgprlemladdrl  7853  caucvgprlemlim  7856  caucvgprprlemml  7869  caucvgprprlemexbt  7881  caucvgprprlemlim  7886  suplocexprlemmu  7893  suplocexprlemloc  7896  suplocexprlemlub  7899  caucvgsrlemgt1  7970  suplocsrlemb  7981  suplocsrlem  7983  axcaucvglemres  8074  xaddval  10029  rebtwn2zlemstep  10459  nn0ltexp2  10918  hashunlem  11013  caucvgre  11478  cvg1nlemres  11482  resqrexlemglsq  11519  maxabslemval  11705  xrmaxiflemcl  11742  xrmaxifle  11743  xrmaxiflemab  11744  xrmaxiflemlub  11745  xrmaxiflemval  11747  xrmaxltsup  11755  divalglemeunn  12418  dvdsbnd  12463  bezoutlemnewy  12503  bezoutlemmain  12505  nninfctlemfo  12547  isprm5lem  12649  ctiunctlemfo  12996  prdsval  13292  sgrpidmndm  13439  mhmmnd  13639  mulgval  13645  txlm  14938  xmettx  15169  txmetcnp  15177  dedekindeu  15282  suplociccreex  15283  dedekindicclemlu  15289  dedekindicclemicc  15291  limcimo  15324  limccnp2cntop  15336  dvply2g  15425  lgsne0  15702