Theorem ad4antlr 745

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  simp-4r  795  ttrcltr  9673  initoeu2  18063  qsidomlem1  21440  cpmatacl  22834  cpmatmcllem  22836  cpmatmcl  22837  chfacfisf  22972  chfacfisfcpmat  22973  restcld  23290  pthaus  23756  txhaus  23765  xkohaus  23771  alexsubALTlem4  24168  ustuqtop3  24361  ulmcau  26516  2sqreulem1  27568  2sqreunnlem1  27571  clwlkclwwlklem2  30260  gsumwun  33309  rhmimaidl  33656  qsdrngi  33694  pidufd  33750  dimkerim  33934  fedgmul  33938  constrfiss  34058  locfinreflem  34147  cmpcref  34157  pstmxmet  34204  sigapildsys  34469  ldgenpisyslem1  34470  signstfvneq0  34876  nn0prpwlem  36695  matunitlindflem1  38127  matunitlindflem2  38128  poimirlem29  38160  heicant  38166  mblfinlem3  38170  mblfinlem4  38171  itg2addnclem2  38183  itg2gt0cn  38186  ftc1cnnc  38203  sstotbnd2  38285  pell1234qrdich  43450  jm2.26lem3  43590  cvgdvgrat  44887  limsupgtlem  46349  limsupub2  46384  xlimmnfv  46406  icccncfext  46459  fourierdlem34  46713  fourierdlem87  46765  etransclem35  46841  smfaddlem1  47335  sfprmdvdsmersenne  48210  sbgoldbwt  48397  bgoldbtbnd  48429  isuspgrim0  48514  ply1mulgsumlem2  49018  nn0sumshdiglemA  49250