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  8368  prdsval  17546  catass  17780  catpropd  17803  cidpropd  17804  subccocl  17940  funcco  17966  natpropd  18074  fucpropd  18075  initoeu2lem1  18109  prfval  18293  xpcpropd  18302  acsfiindd  18647  chnind  18715  chnso  18718  mndpsuppss  18878  mhmmnd  19193  ghmqusnsg  19415  ghmquskerlem3  19419  ghmqusker  19420  omndmul2  20266  drngidl  21454  rhmpreimaidl  21485  rhmqusnsg  21494  isprmidlc  21541  qsidomlem1  21549  qsidomlem2  21550  ssdifidlprm  21555  lindsenlbs  22070  mhpmulcl  22383  psdmul  22400  scmatscm  22741  matunitlindflem1  22907  cpmatmcllem  22949  mptcoe1matfsupp  23033  mp2pm2mplem4  23040  chpdmatlem2  23070  chfacfisf  23085  chfacfisfcpmat  23086  neitr  23411  hauscmplem  23637  trcfilu  24525  cfilucfil  24791  restmetu  24802  metucn  24803  cnheibor  25189  dvlip2  26229  lgamucov  27282  bdayfinbndlem1  28740  tgifscgr  28858  iscgrglt  28864  tgbtwnconn1  28925  legtrd  28939  legtri3  28940  legso  28949  hlcgrex  28969  tglndim0  28984  tglinethru  28991  tglinesseq  28995  colline  29005  tglnpt2  29008  tglnpt4  29010  perpneq  29076  isperp2  29077  footexALT  29080  opphllem  29098  midex  29100  opphllem3  29112  opphllem5  29114  opphllem6  29115  opphl  29117  outpasch  29120  hlpasch  29121  lnopp2hpgb  29128  hpgerlem  29130  lnincplng  29149  plngcplem  29150  plngrotlem1  29152  lnssplnglem  29156  lnssplng  29157  plng3p  29162  lmieu  29176  lnperpex  29196  trgcopy  29198  cgrahl  29222  acopy  29228  tgaaddcpbl  29239  inaghl  29251  cgrg3col4  29259  cgrabasimass  29265  angmgmaddeu1  29266  angmgmaddeu2  29267  angmgmaddeu3  29268  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddrid  29280  prlnghpg  29311  dfprlng2  29312  dfprlng3  29313  perpprlng  29315  prlngex  29316  prlngmolem1  29317  prlngmolem2  29318  quadcgrprlng  29331  f1otrg  29335  nbumgrvtx  29814  3cyclfrgr  30776  numclwlk2lem2f1o  30867  s3f1  33398  ccatws1f1o  33401  dfmgc2  33444  pwrssmgc  33448  mgcf1o  33451  mndlrinvb  33473  gsumwun  33524  psgnfzto1stlem  33548  cycpmrn  33591  tocyccntz  33592  cycpmconjs  33604  isarchi3  33635  archirngz  33637  elrgspnlem2  33691  elrgspnlem4  33693  elrgspnsubrunlem2  33696  erler  33713  rlocaddval  33717  rlocmulval  33718  rloccring  33719  rloc1r  33721  ricdomn1  33737  fracfld  33757  nsgqusf1olem1  33850  nsgqusf1olem2  33851  nsgqusf1olem3  33852  lmhmqusker  33854  rhmquskerlem  33861  elrspunidl  33864  elrspunsn  33865  idlinsubrg  33867  rhmimaidl  33868  mxidlprm  33881  mxidlirredi  33882  mxidlirred  33883  drngmxidlr  33888  opprqusplusg  33899  opprqusmulr  33901  qsdrngi  33905  qsdrng  33907  drnglring  33910  dflring2  33911  dflringlem2  33913  dflringlem3  33914  dflring3  33915  dflring4  33916  rsprprmprmidlb  33941  rprmirred  33949  rprmirredb  33950  rprmdvdsprod  33952  1arithidom  33955  pidufd  33961  1arithufdlem2  33963  1arithufdlem3  33964  1arithufdlem4  33965  dfufd2lem  33967  deg1prod  34001  mplidomlem  34045  mplmulmvr  34057  mplvrpmrhm  34065  psrgsum  34066  psrmonprod  34070  esplyfv  34088  esplyfval1  34091  esplyind  34093  dimkerim  34145  fedgmul  34149  extdg1id  34184  evls1fldgencl  34188  fldextrspunlsplem  34191  fldextrspunlsp  34192  extdgfialglem1  34210  extdgfialg  34212  minplyirred  34229  constrextdg2lem  34266  constrfiss  34269  cos9thpiminplylem2  34301  qtophaus  34354  zarclsint  34390  zarcmplem  34399  esumcst  34581  sigapildsys  34681  oms0  34816  omssubadd  34819  carsgclctunlem3  34839  eulerpartlemgvv  34895  signsply0  35067  signstfvneq0  35088  actfunsnf1o  35120  reprsuc  35131  reprinfz1  35138  breprexplema  35146  breprexplemc  35148  hgt750lemb  35172  cvmlift3lem2  35907  satfdmlem  35955  nn0prpwlem  36949  mblfinlem3  38416  mblfinlem4  38417  itg2addnclem2  38429  itg2gt0cn  38432  ftc1cnnc  38449  ftc1anc  38458  sstotbnd2  38532  lcfl8  42383  aks4d1p8  42961  fldhmf1  42964  mndmolinv  42969  primrootsunit1  42971  primrootscoprmpow  42973  primrootspoweq0  42980  aks6d1c2p2  42993  aks6d1c2lem4  43001  aks6d1c6lem3  43046  aks6d1c7  43058  unitscyglem2  43070  aks5  43078  fiabv  43426  fsuppind  43444  prjspersym  43461  pell1234qrdich  43710  pell14qrdich  43718  pell1qrgap  43723  pellfundex  43735  omabs2  44181  cvgdvgrat  45145  infleinflem2  46208  xrralrecnnle  46220  climrec  46441  climsuse  46446  limcrecl  46467  limsupubuz  46549  limsupgtlem  46613  xlimliminflimsup  46698  fperdvper  46755  dvnprodlem2  46783  etransclem35  47105  hspmbllem2  47463  smflimlem2  47608  smflimlem4  47610  iccpartgt  48335  prproropf1olem4  48414  sfprmdvdsmersenne  48514  gricushgr  48841  2zlidl  49163  ply1mulgsumlem2  49325  nn0sumshdiglemA  49557  imaf1co  50089  uppropd  50115  fuco21  50270  functhinclem4  50381  2arwcat  50534