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  6373  tfrcllemaccex  6386  fimax2gtri  6929  en2eqpr  6935  unsnfidcex  6948  unsnfidcel  6949  ctssdc  7142  cauappcvgprlemloc  7681  caucvgprlemm  7697  caucvgprlemladdrl  7707  caucvgprlemlim  7710  caucvgprprlemml  7723  caucvgprprlemexbt  7735  caucvgprprlemlim  7740  suplocexprlemmu  7747  suplocexprlemloc  7750  suplocexprlemlub  7753  caucvgsrlemgt1  7824  suplocsrlemb  7835  suplocsrlem  7837  axcaucvglemres  7928  xaddval  9875  rebtwn2zlemstep  10283  nn0ltexp2  10721  hashunlem  10816  caucvgre  11022  cvg1nlemres  11026  resqrexlemglsq  11063  maxabslemval  11249  xrmaxiflemcl  11285  xrmaxifle  11286  xrmaxiflemab  11287  xrmaxiflemlub  11288  xrmaxiflemval  11290  xrmaxltsup  11298  divalglemeunn  11958  dvdsbnd  11989  bezoutlemnewy  12029  bezoutlemmain  12031  isprm5lem  12173  ctiunctlemfo  12490  sgrpidmndm  12881  mhmmnd  13058  mulgval  13064  txlm  14236  xmettx  14467  txmetcnp  14475  dedekindeu  14558  suplociccreex  14559  dedekindicclemlu  14565  dedekindicclemicc  14567  limcimo  14591  limccnp2cntop  14603  lgsne0  14897