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  8388  prdsval  17467  catass  17696  catpropd  17719  cidpropd  17720  subccocl  17856  funcco  17882  natpropd  17990  fucpropd  17991  initoeu2lem1  18025  prfval  18209  xpcpropd  18218  acsfiindd  18561  mndpsuppss  18741  mhmmnd  19045  ghmqusnsg  19263  ghmquskerlem3  19267  ghmqusker  19268  rhmpreimaidl  21236  rhmqusnsg  21244  mhpmulcl  22085  psdmul  22102  scmatscm  22449  cpmatmcllem  22654  mptcoe1matfsupp  22738  mp2pm2mplem4  22745  chpdmatlem2  22775  chfacfisf  22790  chfacfisfcpmat  22791  neitr  23116  hauscmplem  23342  trcfilu  24230  cfilucfil  24496  restmetu  24507  metucn  24508  cnheibor  24903  dvlip2  25950  lgamucov  26998  tgifscgr  28433  iscgrglt  28439  tgbtwnconn1  28500  legtrd  28514  legtri3  28515  legso  28524  hlcgrex  28541  tglndim0  28554  tglinethru  28561  tglnpt2  28566  colline  28574  perpneq  28639  isperp2  28640  footexALT  28643  opphllem  28660  midex  28662  opphllem3  28674  opphllem5  28676  opphllem6  28677  opphl  28679  outpasch  28680  hlpasch  28681  lnopp2hpgb  28688  hpgerlem  28690  lmieu  28709  lnperpex  28728  trgcopy  28729  cgrahl  28752  acopy  28758  inaghl  28770  cgrg3col4  28778  f1otrg  28796  nbumgrvtx  29271  3cyclfrgr  30215  numclwlk2lem2f1o  30306  s3f1  32868  ccatws1f1o  32873  dfmgc2  32922  pwrssmgc  32926  mgcf1o  32929  chnind  32937  chnso  32940  mndlrinvb  32966  gsumwun  33005  omndmul2  33026  psgnfzto1stlem  33057  cycpmrn  33100  tocyccntz  33101  cycpmconjs  33113  isarchi3  33131  archirngz  33133  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem2  33189  erler  33206  rlocaddval  33209  rlocmulval  33210  rloccring  33211  rloc1r  33213  fracfld  33248  nsgqusf1olem1  33374  nsgqusf1olem2  33375  nsgqusf1olem3  33376  lmhmqusker  33378  rhmquskerlem  33386  elrspunidl  33389  elrspunsn  33390  idlinsubrg  33392  rhmimaidl  33393  drngidl  33394  isprmidlc  33408  qsidomlem1  33413  qsidomlem2  33414  ssdifidlprm  33419  mxidlprm  33431  mxidlirredi  33432  mxidlirred  33433  drngmxidlr  33439  opprqusplusg  33450  opprqusmulr  33452  qsdrngi  33456  qsdrng  33458  rsprprmprmidlb  33484  rprmirred  33492  rprmirredb  33493  rprmdvdsprod  33495  1arithidom  33498  pidufd  33504  1arithufdlem2  33506  1arithufdlem3  33507  1arithufdlem4  33508  dfufd2lem  33510  dimkerim  33613  fedgmul  33617  extdg1id  33653  evls1fldgencl  33657  fldextrspunlsplem  33660  fldextrspunlsp  33661  minplyirred  33691  constrextdg2lem  33728  constrfiss  33731  cos9thpiminplylem2  33763  qtophaus  33813  zarclsint  33849  zarcmplem  33858  esumcst  34040  sigapildsys  34139  oms0  34275  omssubadd  34278  carsgclctunlem3  34298  eulerpartlemgvv  34354  signsply0  34529  signstfvneq0  34550  actfunsnf1o  34582  reprsuc  34593  reprinfz1  34600  breprexplema  34608  breprexplemc  34610  hgt750lemb  34634  cvmlift3lem2  35288  satfdmlem  35336  nn0prpwlem  36286  lindsenlbs  37585  matunitlindflem1  37586  mblfinlem3  37629  mblfinlem4  37630  itg2addnclem2  37642  itg2gt0cn  37645  ftc1cnnc  37662  ftc1anc  37671  sstotbnd2  37744  lcfl8  41467  aks4d1p8  42046  fldhmf1  42049  mndmolinv  42054  primrootsunit1  42056  primrootscoprmpow  42058  primrootspoweq0  42065  aks6d1c2p2  42078  aks6d1c2lem4  42086  aks6d1c6lem3  42131  aks6d1c7  42143  unitscyglem2  42155  aks5  42163  fiabv  42506  fsuppind  42560  prjspersym  42577  pell1234qrdich  42831  pell14qrdich  42839  pell1qrgap  42844  pellfundex  42856  omabs2  43303  cvgdvgrat  44285  infleinflem2  45346  xrralrecnnle  45358  climrec  45580  climsuse  45585  limcrecl  45606  limsupubuz  45690  limsupgtlem  45754  xlimliminflimsup  45839  fperdvper  45896  dvnprodlem2  45924  etransclem35  46246  hspmbllem2  46604  smflimlem2  46749  smflimlem4  46751  iccpartgt  47389  prproropf1olem4  47468  sfprmdvdsmersenne  47565  gricushgr  47878  2zlidl  48163  ply1mulgsumlem2  48311  nn0sumshdiglemA  48547  imaf1co  49043  fuco21  49195  functhinclem4  49281  2arwcat  49425