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  783  tfrlem1  8414  prdsval  17501  catass  17730  catpropd  17753  cidpropd  17754  subccocl  17895  funcco  17921  natpropd  18032  fucpropd  18033  initoeu2lem1  18067  prfval  18254  xpcpropd  18264  acsfiindd  18610  mndpsuppss  18790  mhmmnd  19094  ghmqusnsg  19312  ghmquskerlem3  19316  ghmqusker  19317  rhmpreimaidl  21304  rhmqusnsg  21312  mhpmulcl  22170  psdmul  22187  scmatscm  22534  cpmatmcllem  22739  mptcoe1matfsupp  22823  mp2pm2mplem4  22830  chpdmatlem2  22860  chfacfisf  22875  chfacfisfcpmat  22876  neitr  23203  hauscmplem  23429  trcfilu  24318  cfilucfil  24587  restmetu  24598  metucn  24599  cnheibor  25000  dvlip2  26048  lgamucov  27095  tgifscgr  28530  iscgrglt  28536  tgbtwnconn1  28597  legtrd  28611  legtri3  28612  legso  28621  hlcgrex  28638  tglndim0  28651  tglinethru  28658  tglnpt2  28663  colline  28671  perpneq  28736  isperp2  28737  footexALT  28740  opphllem  28757  midex  28759  opphllem3  28771  opphllem5  28773  opphllem6  28774  opphl  28776  outpasch  28777  hlpasch  28778  lnopp2hpgb  28785  hpgerlem  28787  lmieu  28806  lnperpex  28825  trgcopy  28826  cgrahl  28849  acopy  28855  inaghl  28867  cgrg3col4  28875  f1otrg  28893  nbumgrvtx  29377  3cyclfrgr  30316  numclwlk2lem2f1o  30407  s3f1  32915  ccatws1f1o  32920  dfmgc2  32970  pwrssmgc  32974  mgcf1o  32977  chnind  32984  chnso  32987  mndlrinvb  33012  gsumwun  33050  omndmul2  33071  psgnfzto1stlem  33102  cycpmrn  33145  tocyccntz  33146  cycpmconjs  33158  isarchi3  33176  archirngz  33178  elrgspnlem2  33232  elrgspnlem4  33234  erler  33251  rlocaddval  33254  rlocmulval  33255  rloccring  33256  rloc1r  33258  fracfld  33289  nsgqusf1olem1  33420  nsgqusf1olem2  33421  nsgqusf1olem3  33422  lmhmqusker  33424  rhmquskerlem  33432  elrspunidl  33435  elrspunsn  33436  idlinsubrg  33438  rhmimaidl  33439  drngidl  33440  isprmidlc  33454  qsidomlem1  33459  qsidomlem2  33460  ssdifidlprm  33465  mxidlprm  33477  mxidlirredi  33478  mxidlirred  33479  drngmxidlr  33485  opprqusplusg  33496  opprqusmulr  33498  qsdrngi  33502  qsdrng  33504  rsprprmprmidlb  33530  rprmirred  33538  rprmirredb  33539  rprmdvdsprod  33541  1arithidom  33544  pidufd  33550  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  dfufd2lem  33556  dimkerim  33654  fedgmul  33658  extdg1id  33690  evls1fldgencl  33694  minplyirred  33718  qtophaus  33796  zarclsint  33832  zarcmplem  33841  esumcst  34043  sigapildsys  34142  oms0  34278  omssubadd  34281  carsgclctunlem3  34301  eulerpartlemgvv  34357  signsply0  34544  signstfvneq0  34565  actfunsnf1o  34597  reprsuc  34608  reprinfz1  34615  breprexplema  34623  breprexplemc  34625  hgt750lemb  34649  cvmlift3lem2  35304  satfdmlem  35352  nn0prpwlem  36304  lindsenlbs  37601  matunitlindflem1  37602  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem2  37658  itg2gt0cn  37661  ftc1cnnc  37678  ftc1anc  37687  sstotbnd2  37760  lcfl8  41484  aks4d1p8  42068  fldhmf1  42071  mndmolinv  42076  primrootsunit1  42078  primrootscoprmpow  42080  primrootspoweq0  42087  aks6d1c2p2  42100  aks6d1c2lem4  42108  aks6d1c6lem3  42153  aks6d1c7  42165  unitscyglem2  42177  aks5  42185  fiabv  42522  fsuppind  42576  prjspersym  42593  pell1234qrdich  42848  pell14qrdich  42856  pell1qrgap  42861  pellfundex  42873  omabs2  43321  cvgdvgrat  44308  infleinflem2  45320  xrralrecnnle  45332  climrec  45558  climsuse  45563  limcrecl  45584  limsupubuz  45668  limsupgtlem  45732  xlimliminflimsup  45817  fperdvper  45874  dvnprodlem2  45902  etransclem35  46224  hspmbllem2  46582  smflimlem2  46727  smflimlem4  46729  iccpartgt  47351  prproropf1olem4  47430  sfprmdvdsmersenne  47527  gricushgr  47823  2zlidl  48083  ply1mulgsumlem2  48232  nn0sumshdiglemA  48468  functhinclem4  48843