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  8416  prdsval  17500  catass  17729  catpropd  17752  cidpropd  17753  subccocl  17890  funcco  17916  natpropd  18024  fucpropd  18025  initoeu2lem1  18059  prfval  18244  xpcpropd  18253  acsfiindd  18598  mndpsuppss  18778  mhmmnd  19082  ghmqusnsg  19300  ghmquskerlem3  19304  ghmqusker  19305  rhmpreimaidl  21287  rhmqusnsg  21295  mhpmulcl  22153  psdmul  22170  scmatscm  22519  cpmatmcllem  22724  mptcoe1matfsupp  22808  mp2pm2mplem4  22815  chpdmatlem2  22845  chfacfisf  22860  chfacfisfcpmat  22861  neitr  23188  hauscmplem  23414  trcfilu  24303  cfilucfil  24572  restmetu  24583  metucn  24584  cnheibor  24987  dvlip2  26034  lgamucov  27081  tgifscgr  28516  iscgrglt  28522  tgbtwnconn1  28583  legtrd  28597  legtri3  28598  legso  28607  hlcgrex  28624  tglndim0  28637  tglinethru  28644  tglnpt2  28649  colline  28657  perpneq  28722  isperp2  28723  footexALT  28726  opphllem  28743  midex  28745  opphllem3  28757  opphllem5  28759  opphllem6  28760  opphl  28762  outpasch  28763  hlpasch  28764  lnopp2hpgb  28771  hpgerlem  28773  lmieu  28792  lnperpex  28811  trgcopy  28812  cgrahl  28835  acopy  28841  inaghl  28853  cgrg3col4  28861  f1otrg  28879  nbumgrvtx  29363  3cyclfrgr  30307  numclwlk2lem2f1o  30398  s3f1  32931  ccatws1f1o  32936  dfmgc2  32986  pwrssmgc  32990  mgcf1o  32993  chnind  33001  chnso  33004  mndlrinvb  33030  gsumwun  33068  omndmul2  33089  psgnfzto1stlem  33120  cycpmrn  33163  tocyccntz  33164  cycpmconjs  33176  isarchi3  33194  archirngz  33196  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem2  33252  erler  33269  rlocaddval  33272  rlocmulval  33273  rloccring  33274  rloc1r  33276  fracfld  33310  nsgqusf1olem1  33441  nsgqusf1olem2  33442  nsgqusf1olem3  33443  lmhmqusker  33445  rhmquskerlem  33453  elrspunidl  33456  elrspunsn  33457  idlinsubrg  33459  rhmimaidl  33460  drngidl  33461  isprmidlc  33475  qsidomlem1  33480  qsidomlem2  33481  ssdifidlprm  33486  mxidlprm  33498  mxidlirredi  33499  mxidlirred  33500  drngmxidlr  33506  opprqusplusg  33517  opprqusmulr  33519  qsdrngi  33523  qsdrng  33525  rsprprmprmidlb  33551  rprmirred  33559  rprmirredb  33560  rprmdvdsprod  33562  1arithidom  33565  pidufd  33571  1arithufdlem2  33573  1arithufdlem3  33574  1arithufdlem4  33575  dfufd2lem  33577  dimkerim  33678  fedgmul  33682  extdg1id  33716  evls1fldgencl  33720  fldextrspunlsplem  33723  fldextrspunlsp  33724  minplyirred  33754  constrextdg2lem  33789  qtophaus  33835  zarclsint  33871  zarcmplem  33880  esumcst  34064  sigapildsys  34163  oms0  34299  omssubadd  34302  carsgclctunlem3  34322  eulerpartlemgvv  34378  signsply0  34566  signstfvneq0  34587  actfunsnf1o  34619  reprsuc  34630  reprinfz1  34637  breprexplema  34645  breprexplemc  34647  hgt750lemb  34671  cvmlift3lem2  35325  satfdmlem  35373  nn0prpwlem  36323  lindsenlbs  37622  matunitlindflem1  37623  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem2  37679  itg2gt0cn  37682  ftc1cnnc  37699  ftc1anc  37708  sstotbnd2  37781  lcfl8  41504  aks4d1p8  42088  fldhmf1  42091  mndmolinv  42096  primrootsunit1  42098  primrootscoprmpow  42100  primrootspoweq0  42107  aks6d1c2p2  42120  aks6d1c2lem4  42128  aks6d1c6lem3  42173  aks6d1c7  42185  unitscyglem2  42197  aks5  42205  fiabv  42546  fsuppind  42600  prjspersym  42617  pell1234qrdich  42872  pell14qrdich  42880  pell1qrgap  42885  pellfundex  42897  omabs2  43345  cvgdvgrat  44332  infleinflem2  45382  xrralrecnnle  45394  climrec  45618  climsuse  45623  limcrecl  45644  limsupubuz  45728  limsupgtlem  45792  xlimliminflimsup  45877  fperdvper  45934  dvnprodlem2  45962  etransclem35  46284  hspmbllem2  46642  smflimlem2  46787  smflimlem4  46789  iccpartgt  47414  prproropf1olem4  47493  sfprmdvdsmersenne  47590  gricushgr  47886  2zlidl  48156  ply1mulgsumlem2  48304  nn0sumshdiglemA  48540  fuco21  49031  functhinclem4  49096