Theorem ad4antlr 723

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem ad4antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 475	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad3antrrr 720	1 ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  initoeu2  17055  cpmatacl  20932  cpmatmcllem  20934  cpmatmcl  20935  chfacfisf  21070  chfacfisfcpmat  21071  restcld  21388  pthaus  21854  txhaus  21863  xkohaus  21869  alexsubALTlem4  22266  ustuqtop3  22459  ulmcau  24590  clwlkclwwlklem2  27384  dimkerim  30445  locfinreflem  30509  cmpcref  30519  pstmxmet  30542  sigapildsys  30827  ldgenpisyslem1  30828  nn0prpwlem  32909  matunitlindflem1  34036  matunitlindflem2  34037  poimirlem29  34069  heicant  34075  mblfinlem3  34079  mblfinlem4  34080  itg2addnclem2  34092  itg2gt0cn  34095  ftc1cnnc  34114  sstotbnd2  34202  pell1234qrdich  38395  jm2.26lem3  38537  cvgdvgrat  39478  limsupgtlem  40927  limsupub2  40962  xlimmnfv  40984  icccncfext  41038  fourierdlem34  41295  fourierdlem87  41347  etransclem35  41423  smfaddlem1  41908  sfprmdvdsmersenne  42551  sbgoldbwt  42700  bgoldbtbnd  42732  ply1mulgsumlem2  43200  nn0sumshdiglemA  43438