Theorem ad4antr 732

Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad4antr	⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem ad4antr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 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:  ad5antr  734  ad5antlr  735  simp-4l  782  tfrlem1  8305  prdsval  17377  catass  17610  catpropd  17633  cidpropd  17634  subccocl  17770  funcco  17796  natpropd  17904  fucpropd  17905  initoeu2lem1  17939  prfval  18123  xpcpropd  18132  acsfiindd  18477  mndpsuppss  18657  mhmmnd  18961  ghmqusnsg  19179  ghmquskerlem3  19183  ghmqusker  19184  omndmul2  20030  rhmpreimaidl  21202  rhmqusnsg  21210  mhpmulcl  22052  psdmul  22069  scmatscm  22416  cpmatmcllem  22621  mptcoe1matfsupp  22705  mp2pm2mplem4  22712  chpdmatlem2  22742  chfacfisf  22757  chfacfisfcpmat  22758  neitr  23083  hauscmplem  23309  trcfilu  24197  cfilucfil  24463  restmetu  24474  metucn  24475  cnheibor  24870  dvlip2  25916  lgamucov  26964  tgifscgr  28471  iscgrglt  28477  tgbtwnconn1  28538  legtrd  28552  legtri3  28553  legso  28562  hlcgrex  28579  tglndim0  28592  tglinethru  28599  tglnpt2  28604  colline  28612  perpneq  28677  isperp2  28678  footexALT  28681  opphllem  28698  midex  28700  opphllem3  28712  opphllem5  28714  opphllem6  28715  opphl  28717  outpasch  28718  hlpasch  28719  lnopp2hpgb  28726  hpgerlem  28728  lmieu  28747  lnperpex  28766  trgcopy  28767  cgrahl  28790  acopy  28796  inaghl  28808  cgrg3col4  28816  f1otrg  28834  nbumgrvtx  29309  3cyclfrgr  30250  numclwlk2lem2f1o  30341  s3f1  32901  ccatws1f1o  32906  dfmgc2  32951  pwrssmgc  32955  mgcf1o  32958  chnind  32966  chnso  32969  mndlrinvb  32992  gsumwun  33031  psgnfzto1stlem  33055  cycpmrn  33098  tocyccntz  33099  cycpmconjs  33111  isarchi3  33142  archirngz  33144  elrgspnlem2  33196  elrgspnlem4  33198  elrgspnsubrunlem2  33201  erler  33218  rlocaddval  33221  rlocmulval  33222  rloccring  33223  rloc1r  33225  fracfld  33260  nsgqusf1olem1  33363  nsgqusf1olem2  33364  nsgqusf1olem3  33365  lmhmqusker  33367  rhmquskerlem  33375  elrspunidl  33378  elrspunsn  33379  idlinsubrg  33381  rhmimaidl  33382  drngidl  33383  isprmidlc  33397  qsidomlem1  33402  qsidomlem2  33403  ssdifidlprm  33408  mxidlprm  33420  mxidlirredi  33421  mxidlirred  33422  drngmxidlr  33428  opprqusplusg  33439  opprqusmulr  33441  qsdrngi  33445  qsdrng  33447  rsprprmprmidlb  33473  rprmirred  33481  rprmirredb  33482  rprmdvdsprod  33484  1arithidom  33487  pidufd  33493  1arithufdlem2  33495  1arithufdlem3  33496  1arithufdlem4  33497  dfufd2lem  33499  dimkerim  33602  fedgmul  33606  extdg1id  33640  evls1fldgencl  33644  fldextrspunlsplem  33647  fldextrspunlsp  33648  minplyirred  33680  constrextdg2lem  33717  constrfiss  33720  cos9thpiminplylem2  33752  qtophaus  33805  zarclsint  33841  zarcmplem  33850  esumcst  34032  sigapildsys  34131  oms0  34267  omssubadd  34270  carsgclctunlem3  34290  eulerpartlemgvv  34346  signsply0  34521  signstfvneq0  34542  actfunsnf1o  34574  reprsuc  34585  reprinfz1  34592  breprexplema  34600  breprexplemc  34602  hgt750lemb  34626  cvmlift3lem2  35295  satfdmlem  35343  nn0prpwlem  36298  lindsenlbs  37597  matunitlindflem1  37598  mblfinlem3  37641  mblfinlem4  37642  itg2addnclem2  37654  itg2gt0cn  37657  ftc1cnnc  37674  ftc1anc  37683  sstotbnd2  37756  lcfl8  41484  aks4d1p8  42063  fldhmf1  42066  mndmolinv  42071  primrootsunit1  42073  primrootscoprmpow  42075  primrootspoweq0  42082  aks6d1c2p2  42095  aks6d1c2lem4  42103  aks6d1c6lem3  42148  aks6d1c7  42160  unitscyglem2  42172  aks5  42180  fiabv  42512  fsuppind  42566  prjspersym  42583  pell1234qrdich  42837  pell14qrdich  42845  pell1qrgap  42850  pellfundex  42862  omabs2  43308  cvgdvgrat  44289  infleinflem2  45354  xrralrecnnle  45366  climrec  45588  climsuse  45593  limcrecl  45614  limsupubuz  45698  limsupgtlem  45762  xlimliminflimsup  45847  fperdvper  45904  dvnprodlem2  45932  etransclem35  46254  hspmbllem2  46612  smflimlem2  46757  smflimlem4  46759  iccpartgt  47415  prproropf1olem4  47494  sfprmdvdsmersenne  47591  gricushgr  47905  2zlidl  48228  ply1mulgsumlem2  48376  nn0sumshdiglemA  48608  imaf1co  49144  uppropd  49170  fuco21  49325  functhinclem4  49436  2arwcat  49589