Theorem ad4antlr 769

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad4antlr	⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ad3antlr 767	. 2 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
3	2	adantr 481	1 ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  ad5antlr  771  initoeu2  16666  cpmatacl  20521  cpmatmcllem  20523  cpmatmcl  20524  chfacfisf  20659  chfacfisfcpmat  20660  restcld  20976  pthaus  21441  txhaus  21450  xkohaus  21456  alexsubALTlem4  21854  ustuqtop3  22047  ulmcau  24149  clwlkclwwlklem2  26901  locfinreflem  29907  cmpcref  29917  pstmxmet  29940  sigapildsys  30225  ldgenpisyslem1  30226  nn0prpwlem  32317  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem29  33438  heicant  33444  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem2  33462  itg2gt0cn  33465  ftc1cnnc  33484  sstotbnd2  33573  pell1234qrdich  37425  jm2.26lem3  37568  cvgdvgrat  38512  limsupgtlem  40009  xlimmnfv  40060  icccncfext  40100  fourierdlem34  40358  fourierdlem87  40410  etransclem35  40486  smfaddlem1  40971  sfprmdvdsmersenne  41520  sbgoldbwt  41665  bgoldbtbnd  41697  ply1mulgsumlem2  42175  nn0sumshdiglemA  42413