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  6578  tfrcllemaccex  6591  fimax2gtri  7158  en2eqpr  7166  unsnfidcex  7179  unsnfidcel  7180  fissfi  7215  ctssdc  7403  cauappcvgprlemloc  7966  caucvgprlemm  7982  caucvgprlemladdrl  7992  caucvgprlemlim  7995  caucvgprprlemml  8008  caucvgprprlemexbt  8020  caucvgprprlemlim  8025  suplocexprlemmu  8032  suplocexprlemloc  8035  suplocexprlemlub  8038  caucvgsrlemgt1  8109  suplocsrlemb  8120  suplocsrlem  8122  axcaucvglemres  8213  xaddval  10177  rebtwn2zlemstep  10611  nn0ltexp2  11070  hashunlem  11166  caucvgre  11662  cvg1nlemres  11666  resqrexlemglsq  11703  maxabslemval  11889  xrmaxiflemcl  11926  xrmaxifle  11927  xrmaxiflemab  11928  xrmaxiflemlub  11929  xrmaxiflemval  11931  xrmaxltsup  11939  divalglemeunn  12603  dvdsbnd  12648  bezoutlemnewy  12688  bezoutlemmain  12690  nninfctlemfo  12732  isprm5lem  12834  ctiunctlemfo  13182  prdsval  13478  sgrpidmndm  13625  mhmmnd  13825  mulgval  13831  txlm  15136  xmettx  15367  txmetcnp  15375  dedekindeu  15480  suplociccreex  15481  dedekindicclemlu  15487  dedekindicclemicc  15489  limcimo  15522  limccnp2cntop  15534  dvply2g  15623  lgsne0  15903  gfsumval  16853  gfsumz  16860