Theorem ad4antlr 733

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simp-4r  783  ttrcltr  9676  initoeu2  17985  cpmatacl  22610  cpmatmcllem  22612  cpmatmcl  22613  chfacfisf  22748  chfacfisfcpmat  22749  restcld  23066  pthaus  23532  txhaus  23541  xkohaus  23547  alexsubALTlem4  23944  ustuqtop3  24138  ulmcau  26311  2sqreulem1  27364  2sqreunnlem1  27367  clwlkclwwlklem2  29936  gsumwun  33012  rhmimaidl  33410  qsidomlem1  33430  qsdrngi  33473  pidufd  33521  dimkerim  33630  fedgmul  33634  constrfiss  33748  locfinreflem  33837  cmpcref  33847  pstmxmet  33894  sigapildsys  34159  ldgenpisyslem1  34160  signstfvneq0  34570  nn0prpwlem  36317  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem29  37650  heicant  37656  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem2  37673  itg2gt0cn  37676  ftc1cnnc  37693  sstotbnd2  37775  pell1234qrdich  42856  jm2.26lem3  42997  cvgdvgrat  44309  limsupgtlem  45782  limsupub2  45817  xlimmnfv  45839  icccncfext  45892  fourierdlem34  46146  fourierdlem87  46198  etransclem35  46274  smfaddlem1  46768  sfprmdvdsmersenne  47608  sbgoldbwt  47782  bgoldbtbnd  47814  isuspgrim0  47898  ply1mulgsumlem2  48380  nn0sumshdiglemA  48612