Theorem ad4antr 745

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5antr  747  ad5antlr  748  simp-4l  795  tfrlem1  8414  prdsval  17658  catass  17892  catpropd  17915  cidpropd  17916  subccocl  18052  funcco  18078  natpropd  18186  fucpropd  18187  initoeu2lem1  18221  prfval  18405  xpcpropd  18414  acsfiindd  18759  chnind  18827  chnso  18830  mndpsuppss  18991  mhmmnd  19306  ghmqusnsg  19529  ghmquskerlem3  19533  ghmqusker  19534  omndmul2  20380  drngidl  21572  rhmpreimaidl  21604  rhmqusnsg  21614  isprmidlc  21661  qsidomlem1  21669  qsidomlem2  21670  ssdifidlprm  21675  lindsenlbs  22190  mhpmulcl  22503  psdmul  22520  scmatscm  22861  matunitlindflem1  23027  cpmatmcllem  23069  mptcoe1matfsupp  23153  mp2pm2mplem4  23160  chpdmatlem2  23190  chfacfisf  23205  chfacfisfcpmat  23206  neitr  23531  hauscmplem  23757  trcfilu  24645  cfilucfil  24911  restmetu  24922  metucn  24923  cnheibor  25309  dvlip2  26348  lgamucov  27398  bdayfinbndlem1  28886  tgifscgr  29004  iscgrglt  29010  tgbtwnconn1  29071  legtrd  29085  legtri3  29086  legso  29095  hlcgrex  29115  tglndim0  29130  tglinethru  29137  tglinesseq  29141  colline  29151  tglnpt2  29154  tglnpt4  29156  perpneq  29222  isperp2  29223  footexALT  29226  opphllem  29244  midex  29246  opphllem3  29258  opphllem5  29260  opphllem6  29261  opphl  29263  outpasch  29266  hlpasch  29267  lnopp2hpgb  29274  hpgerlem  29276  lnincplng  29295  plngcplem  29296  plngrotlem1  29298  lnssplnglem  29302  lnssplng  29303  plng3p  29308  lmieu  29322  lnperpex  29342  trgcopy  29344  cgrahl  29368  acopy  29374  tgaaddcpbl  29385  inaghl  29397  cgrg3col4  29405  cgrabasimass  29411  angmgmaddeu1  29412  angmgmaddeu2  29413  angmgmaddeu3  29414  angmgmaddcpbl  29423  angmgmaddcl  29424  angmgmaddrid  29426  prlnghpg  29457  dfprlng2  29458  dfprlng3  29459  perpprlng  29461  prlngex  29462  prlngmolem1  29463  prlngmolem2  29464  quadcgrprlng  29477  f1otrg  29481  nbumgrvtx  29960  3cyclfrgr  30922  numclwlk2lem2f1o  31013  s3f1  33584  ccatws1f1o  33587  dfmgc2  33633  pwrssmgc  33637  mgcf1o  33640  mndlrinvb  33662  gsumwun  33713  psgnfzto1stlem  33737  cycpmrn  33780  tocyccntz  33781  cycpmconjs  33793  isarchi3  33824  archirngz  33826  elrgspnlem2  33880  elrgspnlem4  33882  elrgspnsubrunlem2  33885  erler  33902  rlocaddval  33906  rlocmulval  33907  rloccring  33908  rloc1r  33910  ricdomn1  33926  edompidlem  33940  fracfld  33954  nsgqusf1olem1  34048  nsgqusf1olem2  34049  nsgqusf1olem3  34050  lmhmqusker  34052  rhmquskerlem  34059  elrspunidl  34062  elrspunsn  34063  idlinsubrg  34065  rhmimaidl  34066  mxidlprm  34079  mxidlirredi  34080  mxidlirred  34081  drngmxidlr  34086  opprqusplusg  34097  opprqusmulr  34099  qsdrngi  34103  qsdrng  34105  drnglring  34108  dflring2  34109  dflringlem2  34111  dflringlem3  34112  dflring3  34113  dflring4  34114  rsprprmprmidlb  34139  rprmirred  34147  rprmirredb  34148  rprmdvdsprod  34150  1arithidom  34153  pidufd  34159  1arithufdlem2  34161  1arithufdlem3  34162  1arithufdlem4  34163  dfufd2lem  34165  deg1prod  34198  mplidomlem  34242  mplmulmvr  34254  mplvrpmrhm  34262  psrgsum  34263  psrmonprod  34267  esplyfv  34285  esplyfval1  34288  esplyind  34290  dimkerim  34342  fedgmul  34346  extdg1id  34381  evls1fldgencl  34385  fldextrspunlsplem  34388  fldextrspunlsp  34389  extdgfialglem1  34407  extdgfialg  34409  minplyirred  34426  constrextdg2lem  34463  constrfiss  34466  cos9thpiminplylem2  34498  qtophaus  34551  zarclsint  34587  zarcmplem  34596  esumcst  34778  sigapildsys  34878  oms0  35012  omssubadd  35015  carsgclctunlem3  35035  eulerpartlemgvv  35091  signsply0  35263  signstfvneq0  35284  actfunsnf1o  35316  reprsuc  35327  reprinfz1  35334  breprexplema  35342  breprexplemc  35344  hgt750lemb  35368  cvmlift3lem2  36265  satfdmlem  36313  nn0prpwlem  37301  mh-inf3f1  37520  mblfinlem3  38782  mblfinlem4  38783  itg2addnclem2  38795  itg2gt0cn  38798  ftc1cnnc  38815  ftc1anc  38824  sstotbnd2  38911  lcfl8  42762  aks4d1p8  43340  fldhmf1  43343  mndmolinv  43348  primrootsunit1  43350  primrootscoprmpow  43352  primrootspoweq0  43359  aks6d1c2p2  43372  aks6d1c2lem4  43380  aks6d1c6lem3  43425  aks6d1c7  43437  unitscyglem2  43449  aks5  43457  fiabv  43804  fsuppind  43822  prjspersym  43839  pell1234qrdich  44072  pell14qrdich  44080  pell1qrgap  44085  pellfundex  44097  omabs2  44537  cvgdvgrat  45500  infleinflem2  46597  xrralrecnnle  46609  climrec  46830  climsuse  46835  limcrecl  46856  limsupubuz  46938  limsupgtlem  47002  xlimliminflimsup  47087  fperdvper  47144  dvnprodlem2  47172  etransclem35  47494  hspmbllem2  47852  smflimlem2  47997  smflimlem4  47999  iccpartgt  48724  prproropf1olem4  48803  sfprmdvdsmersenne  48903  gricushgr  49230  2zlidl  49552  ply1mulgsumlem2  49714  nn0sumshdiglemA  49946  imaf1co  50486  uppropd  50512  fuco21  50673  functhinclem4  50797  2arwcat  50953