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  9730  initoeu2  18029  cpmatacl  22654  cpmatmcllem  22656  cpmatmcl  22657  chfacfisf  22792  chfacfisfcpmat  22793  restcld  23110  pthaus  23576  txhaus  23585  xkohaus  23591  alexsubALTlem4  23988  ustuqtop3  24182  ulmcau  26356  2sqreulem1  27409  2sqreunnlem1  27412  clwlkclwwlklem2  29981  gsumwun  33059  rhmimaidl  33447  qsidomlem1  33467  qsdrngi  33510  pidufd  33558  dimkerim  33667  fedgmul  33671  constrfiss  33785  locfinreflem  33871  cmpcref  33881  pstmxmet  33928  sigapildsys  34193  ldgenpisyslem1  34194  signstfvneq0  34604  nn0prpwlem  36340  matunitlindflem1  37640  matunitlindflem2  37641  poimirlem29  37673  heicant  37679  mblfinlem3  37683  mblfinlem4  37684  itg2addnclem2  37696  itg2gt0cn  37699  ftc1cnnc  37716  sstotbnd2  37798  pell1234qrdich  42884  jm2.26lem3  43025  cvgdvgrat  44337  limsupgtlem  45806  limsupub2  45841  xlimmnfv  45863  icccncfext  45916  fourierdlem34  46170  fourierdlem87  46222  etransclem35  46298  smfaddlem1  46792  sfprmdvdsmersenne  47617  sbgoldbwt  47791  bgoldbtbnd  47823  isuspgrim0  47907  ply1mulgsumlem2  48363  nn0sumshdiglemA  48599