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  9613  initoeu2  17925  cpmatacl  22632  cpmatmcllem  22634  cpmatmcl  22635  chfacfisf  22770  chfacfisfcpmat  22771  restcld  23088  pthaus  23554  txhaus  23563  xkohaus  23569  alexsubALTlem4  23966  ustuqtop3  24159  ulmcau  26332  2sqreulem1  27385  2sqreunnlem1  27388  clwlkclwwlklem2  29982  gsumwun  33052  rhmimaidl  33404  qsidomlem1  33424  qsdrngi  33467  pidufd  33515  dimkerim  33661  fedgmul  33665  constrfiss  33785  locfinreflem  33874  cmpcref  33884  pstmxmet  33931  sigapildsys  34196  ldgenpisyslem1  34197  signstfvneq0  34606  nn0prpwlem  36387  matunitlindflem1  37676  matunitlindflem2  37677  poimirlem29  37709  heicant  37715  mblfinlem3  37719  mblfinlem4  37720  itg2addnclem2  37732  itg2gt0cn  37735  ftc1cnnc  37752  sstotbnd2  37834  pell1234qrdich  42978  jm2.26lem3  43118  cvgdvgrat  44430  limsupgtlem  45899  limsupub2  45934  xlimmnfv  45956  icccncfext  46009  fourierdlem34  46263  fourierdlem87  46315  etransclem35  46391  smfaddlem1  46885  sfprmdvdsmersenne  47727  sbgoldbwt  47901  bgoldbtbnd  47933  isuspgrim0  48018  ply1mulgsumlem2  48512  nn0sumshdiglemA  48744