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  6579  tfrcllemaccex  6592  fimax2gtri  7159  en2eqpr  7167  unsnfidcex  7180  unsnfidcel  7181  fissfi  7216  ctssdc  7404  cauappcvgprlemloc  7967  caucvgprlemm  7983  caucvgprlemladdrl  7993  caucvgprlemlim  7996  caucvgprprlemml  8009  caucvgprprlemexbt  8021  caucvgprprlemlim  8026  suplocexprlemmu  8033  suplocexprlemloc  8036  suplocexprlemlub  8039  caucvgsrlemgt1  8110  suplocsrlemb  8121  suplocsrlem  8123  axcaucvglemres  8214  xaddval  10178  rebtwn2zlemstep  10612  nn0ltexp2  11071  hashunlem  11168  caucvgre  11664  cvg1nlemres  11668  resqrexlemglsq  11705  maxabslemval  11891  xrmaxiflemcl  11928  xrmaxifle  11929  xrmaxiflemab  11930  xrmaxiflemlub  11931  xrmaxiflemval  11933  xrmaxltsup  11941  divalglemeunn  12605  dvdsbnd  12650  bezoutlemnewy  12690  bezoutlemmain  12692  nninfctlemfo  12734  isprm5lem  12836  ctiunctlemfo  13188  prdsval  13484  sgrpidmndm  13631  mhmmnd  13831  mulgval  13837  txlm  15142  xmettx  15373  txmetcnp  15381  dedekindeu  15486  suplociccreex  15487  dedekindicclemlu  15493  dedekindicclemicc  15495  limcimo  15528  limccnp2cntop  15540  dvply2g  15629  lgsne0  15909  gfsumval  16860  gfsumz  16867