Theorem ad4antlr 731

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 484	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad3antrrr 728	1 ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simp-4r  782  initoeu2  17278  cpmatacl  21326  cpmatmcllem  21328  cpmatmcl  21329  chfacfisf  21464  chfacfisfcpmat  21465  restcld  21782  pthaus  22248  txhaus  22257  xkohaus  22263  alexsubALTlem4  22660  ustuqtop3  22854  ulmcau  24985  2sqreulem1  26024  2sqreunnlem1  26027  clwlkclwwlklem2  27780  qsidomlem1  30967  dimkerim  31025  fedgmul  31029  locfinreflem  31106  cmpcref  31116  pstmxmet  31139  sigapildsys  31423  ldgenpisyslem1  31424  signstfvneq0  31844  nn0prpwlem  33672  matunitlindflem1  34890  matunitlindflem2  34891  poimirlem29  34923  heicant  34929  mblfinlem3  34933  mblfinlem4  34934  itg2addnclem2  34946  itg2gt0cn  34949  ftc1cnnc  34968  sstotbnd2  35054  pell1234qrdich  39465  jm2.26lem3  39605  cvgdvgrat  40652  limsupgtlem  42065  limsupub2  42100  xlimmnfv  42122  icccncfext  42177  fourierdlem34  42433  fourierdlem87  42485  etransclem35  42561  smfaddlem1  43046  sfprmdvdsmersenne  43775  sbgoldbwt  43949  bgoldbtbnd  43981  ply1mulgsumlem2  44448  nn0sumshdiglemA  44686