Theorem ad4antlr 739

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  simp-4r  789  ttrcltr  9635  initoeu2  17981  cpmatacl  22706  cpmatmcllem  22708  cpmatmcl  22709  chfacfisf  22844  chfacfisfcpmat  22845  restcld  23162  pthaus  23628  txhaus  23637  xkohaus  23643  alexsubALTlem4  24040  ustuqtop3  24233  ulmcau  26385  2sqreulem1  27434  2sqreunnlem1  27437  clwlkclwwlklem2  30095  gsumwun  33164  rhmimaidl  33522  qsidomlem1  33542  qsdrngi  33585  pidufd  33633  dimkerim  33818  fedgmul  33822  constrfiss  33942  locfinreflem  34031  cmpcref  34041  pstmxmet  34088  sigapildsys  34353  ldgenpisyslem1  34354  signstfvneq0  34763  nn0prpwlem  36557  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem29  38023  heicant  38029  mblfinlem3  38033  mblfinlem4  38034  itg2addnclem2  38046  itg2gt0cn  38049  ftc1cnnc  38066  sstotbnd2  38148  pell1234qrdich  43313  jm2.26lem3  43453  cvgdvgrat  44764  limsupgtlem  46227  limsupub2  46262  xlimmnfv  46284  icccncfext  46337  fourierdlem34  46591  fourierdlem87  46643  etransclem35  46719  smfaddlem1  47213  sfprmdvdsmersenne  48088  sbgoldbwt  48275  bgoldbtbnd  48307  isuspgrim0  48392  ply1mulgsumlem2  48885  nn0sumshdiglemA  49117