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  6403  tfrcllemaccex  6416  fimax2gtri  6959  en2eqpr  6965  unsnfidcex  6978  unsnfidcel  6979  ctssdc  7174  cauappcvgprlemloc  7714  caucvgprlemm  7730  caucvgprlemladdrl  7740  caucvgprlemlim  7743  caucvgprprlemml  7756  caucvgprprlemexbt  7768  caucvgprprlemlim  7773  suplocexprlemmu  7780  suplocexprlemloc  7783  suplocexprlemlub  7786  caucvgsrlemgt1  7857  suplocsrlemb  7868  suplocsrlem  7870  axcaucvglemres  7961  xaddval  9914  rebtwn2zlemstep  10324  nn0ltexp2  10783  hashunlem  10878  caucvgre  11128  cvg1nlemres  11132  resqrexlemglsq  11169  maxabslemval  11355  xrmaxiflemcl  11391  xrmaxifle  11392  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxiflemval  11396  xrmaxltsup  11404  divalglemeunn  12065  dvdsbnd  12096  bezoutlemnewy  12136  bezoutlemmain  12138  nninfctlemfo  12180  isprm5lem  12282  ctiunctlemfo  12599  sgrpidmndm  13004  mhmmnd  13189  mulgval  13195  txlm  14458  xmettx  14689  txmetcnp  14697  dedekindeu  14802  suplociccreex  14803  dedekindicclemlu  14809  dedekindicclemicc  14811  limcimo  14844  limccnp2cntop  14856  lgsne0  15195