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  8295  prdsval  17359  catass  17592  catpropd  17615  cidpropd  17616  subccocl  17752  funcco  17778  natpropd  17886  fucpropd  17887  initoeu2lem1  17921  prfval  18105  xpcpropd  18114  acsfiindd  18459  chnind  18527  chnso  18530  mndpsuppss  18673  mhmmnd  18977  ghmqusnsg  19195  ghmquskerlem3  19199  ghmqusker  19200  omndmul2  20046  rhmpreimaidl  21215  rhmqusnsg  21223  mhpmulcl  22065  psdmul  22082  scmatscm  22429  cpmatmcllem  22634  mptcoe1matfsupp  22718  mp2pm2mplem4  22725  chpdmatlem2  22755  chfacfisf  22770  chfacfisfcpmat  22771  neitr  23096  hauscmplem  23322  trcfilu  24209  cfilucfil  24475  restmetu  24486  metucn  24487  cnheibor  24882  dvlip2  25928  lgamucov  26976  tgifscgr  28487  iscgrglt  28493  tgbtwnconn1  28554  legtrd  28568  legtri3  28569  legso  28578  hlcgrex  28595  tglndim0  28608  tglinethru  28615  tglnpt2  28620  colline  28628  perpneq  28693  isperp2  28694  footexALT  28697  opphllem  28714  midex  28716  opphllem3  28728  opphllem5  28730  opphllem6  28731  opphl  28733  outpasch  28734  hlpasch  28735  lnopp2hpgb  28742  hpgerlem  28744  lmieu  28763  lnperpex  28782  trgcopy  28783  cgrahl  28806  acopy  28812  inaghl  28824  cgrg3col4  28832  f1otrg  28850  nbumgrvtx  29325  3cyclfrgr  30266  numclwlk2lem2f1o  30357  s3f1  32926  ccatws1f1o  32930  dfmgc2  32975  pwrssmgc  32979  mgcf1o  32982  mndlrinvb  33004  gsumwun  33043  psgnfzto1stlem  33067  cycpmrn  33110  tocyccntz  33111  cycpmconjs  33123  isarchi3  33154  archirngz  33156  elrgspnlem2  33208  elrgspnlem4  33210  elrgspnsubrunlem2  33213  erler  33230  rlocaddval  33233  rlocmulval  33234  rloccring  33235  rloc1r  33237  fracfld  33272  nsgqusf1olem1  33376  nsgqusf1olem2  33377  nsgqusf1olem3  33378  lmhmqusker  33380  rhmquskerlem  33388  elrspunidl  33391  elrspunsn  33392  idlinsubrg  33394  rhmimaidl  33395  drngidl  33396  isprmidlc  33410  qsidomlem1  33415  qsidomlem2  33416  ssdifidlprm  33421  mxidlprm  33433  mxidlirredi  33434  mxidlirred  33435  drngmxidlr  33441  opprqusplusg  33452  opprqusmulr  33454  qsdrngi  33458  qsdrng  33460  rsprprmprmidlb  33486  rprmirred  33494  rprmirredb  33495  rprmdvdsprod  33497  1arithidom  33500  pidufd  33506  1arithufdlem2  33508  1arithufdlem3  33509  1arithufdlem4  33510  dfufd2lem  33512  mplvrpmrhm  33575  esplyfv  33589  dimkerim  33638  fedgmul  33642  extdg1id  33677  evls1fldgencl  33681  fldextrspunlsplem  33684  fldextrspunlsp  33685  extdgfialglem1  33703  extdgfialg  33705  minplyirred  33722  constrextdg2lem  33759  constrfiss  33762  cos9thpiminplylem2  33794  qtophaus  33847  zarclsint  33883  zarcmplem  33892  esumcst  34074  sigapildsys  34173  oms0  34308  omssubadd  34311  carsgclctunlem3  34331  eulerpartlemgvv  34387  signsply0  34562  signstfvneq0  34583  actfunsnf1o  34615  reprsuc  34626  reprinfz1  34633  breprexplema  34641  breprexplemc  34643  hgt750lemb  34667  cvmlift3lem2  35362  satfdmlem  35410  nn0prpwlem  36362  lindsenlbs  37661  matunitlindflem1  37662  mblfinlem3  37705  mblfinlem4  37706  itg2addnclem2  37718  itg2gt0cn  37721  ftc1cnnc  37738  ftc1anc  37747  sstotbnd2  37820  lcfl8  41547  aks4d1p8  42126  fldhmf1  42129  mndmolinv  42134  primrootsunit1  42136  primrootscoprmpow  42138  primrootspoweq0  42145  aks6d1c2p2  42158  aks6d1c2lem4  42166  aks6d1c6lem3  42211  aks6d1c7  42223  unitscyglem2  42235  aks5  42243  fiabv  42575  fsuppind  42629  prjspersym  42646  pell1234qrdich  42900  pell14qrdich  42908  pell1qrgap  42913  pellfundex  42925  omabs2  43371  cvgdvgrat  44352  infleinflem2  45415  xrralrecnnle  45427  climrec  45649  climsuse  45654  limcrecl  45675  limsupubuz  45757  limsupgtlem  45821  xlimliminflimsup  45906  fperdvper  45963  dvnprodlem2  45991  etransclem35  46313  hspmbllem2  46671  smflimlem2  46816  smflimlem4  46818  iccpartgt  47464  prproropf1olem4  47543  sfprmdvdsmersenne  47640  gricushgr  47954  2zlidl  48277  ply1mulgsumlem2  48425  nn0sumshdiglemA  48657  imaf1co  49193  uppropd  49219  fuco21  49374  functhinclem4  49485  2arwcat  49638