Theorem ad4antr 733

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 731	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  735  ad5antlr  736  simp-4l  783  tfrlem1  8308  prdsval  17409  catass  17643  catpropd  17666  cidpropd  17667  subccocl  17803  funcco  17829  natpropd  17937  fucpropd  17938  initoeu2lem1  17972  prfval  18156  xpcpropd  18165  acsfiindd  18510  chnind  18578  chnso  18581  mndpsuppss  18724  mhmmnd  19031  ghmqusnsg  19248  ghmquskerlem3  19252  ghmqusker  19253  omndmul2  20099  rhmpreimaidl  21267  rhmqusnsg  21275  mhpmulcl  22125  psdmul  22142  scmatscm  22488  cpmatmcllem  22693  mptcoe1matfsupp  22777  mp2pm2mplem4  22784  chpdmatlem2  22814  chfacfisf  22829  chfacfisfcpmat  22830  neitr  23155  hauscmplem  23381  trcfilu  24268  cfilucfil  24534  restmetu  24545  metucn  24546  cnheibor  24932  dvlip2  25972  lgamucov  27015  bdayfinbndlem1  28473  tgifscgr  28590  iscgrglt  28596  tgbtwnconn1  28657  legtrd  28671  legtri3  28672  legso  28681  hlcgrex  28698  tglndim0  28711  tglinethru  28718  tglnpt2  28723  colline  28731  perpneq  28796  isperp2  28797  footexALT  28800  opphllem  28817  midex  28819  opphllem3  28831  opphllem5  28833  opphllem6  28834  opphl  28836  outpasch  28837  hlpasch  28838  lnopp2hpgb  28845  hpgerlem  28847  lmieu  28866  lnperpex  28885  trgcopy  28886  cgrahl  28909  acopy  28915  inaghl  28927  cgrg3col4  28935  f1otrg  28953  nbumgrvtx  29429  3cyclfrgr  30373  numclwlk2lem2f1o  30464  s3f1  33022  ccatws1f1o  33026  dfmgc2  33071  pwrssmgc  33075  mgcf1o  33078  mndlrinvb  33100  gsumwun  33152  psgnfzto1stlem  33176  cycpmrn  33219  tocyccntz  33220  cycpmconjs  33232  isarchi3  33263  archirngz  33265  elrgspnlem2  33319  elrgspnlem4  33321  elrgspnsubrunlem2  33324  erler  33341  rlocaddval  33344  rlocmulval  33345  rloccring  33346  rloc1r  33348  fracfld  33384  nsgqusf1olem1  33488  nsgqusf1olem2  33489  nsgqusf1olem3  33490  lmhmqusker  33492  rhmquskerlem  33500  elrspunidl  33503  elrspunsn  33504  idlinsubrg  33506  rhmimaidl  33507  drngidl  33508  isprmidlc  33522  qsidomlem1  33527  qsidomlem2  33528  ssdifidlprm  33533  mxidlprm  33545  mxidlirredi  33546  mxidlirred  33547  drngmxidlr  33553  opprqusplusg  33564  opprqusmulr  33566  qsdrngi  33570  qsdrng  33572  rsprprmprmidlb  33598  rprmirred  33606  rprmirredb  33607  rprmdvdsprod  33609  1arithidom  33612  pidufd  33618  1arithufdlem2  33620  1arithufdlem3  33621  1arithufdlem4  33622  dfufd2lem  33624  deg1prod  33658  mplmulmvr  33698  mplvrpmrhm  33706  psrgsum  33707  psrmonprod  33711  esplyfv  33729  esplyfval1  33732  esplyind  33734  dimkerim  33787  fedgmul  33791  extdg1id  33826  evls1fldgencl  33830  fldextrspunlsplem  33833  fldextrspunlsp  33834  extdgfialglem1  33852  extdgfialg  33854  minplyirred  33871  constrextdg2lem  33908  constrfiss  33911  cos9thpiminplylem2  33943  qtophaus  33996  zarclsint  34032  zarcmplem  34041  esumcst  34223  sigapildsys  34322  oms0  34457  omssubadd  34460  carsgclctunlem3  34480  eulerpartlemgvv  34536  signsply0  34711  signstfvneq0  34732  actfunsnf1o  34764  reprsuc  34775  reprinfz1  34782  breprexplema  34790  breprexplemc  34792  hgt750lemb  34816  cvmlift3lem2  35518  satfdmlem  35566  nn0prpwlem  36520  lindsenlbs  37950  matunitlindflem1  37951  mblfinlem3  37994  mblfinlem4  37995  itg2addnclem2  38007  itg2gt0cn  38010  ftc1cnnc  38027  ftc1anc  38036  sstotbnd2  38109  lcfl8  41962  aks4d1p8  42540  fldhmf1  42543  mndmolinv  42548  primrootsunit1  42550  primrootscoprmpow  42552  primrootspoweq0  42559  aks6d1c2p2  42572  aks6d1c2lem4  42580  aks6d1c6lem3  42625  aks6d1c7  42637  unitscyglem2  42649  aks5  42657  fiabv  42995  fsuppind  43037  prjspersym  43054  pell1234qrdich  43307  pell14qrdich  43315  pell1qrgap  43320  pellfundex  43332  omabs2  43778  cvgdvgrat  44758  infleinflem2  45818  xrralrecnnle  45830  climrec  46051  climsuse  46056  limcrecl  46077  limsupubuz  46159  limsupgtlem  46223  xlimliminflimsup  46308  fperdvper  46365  dvnprodlem2  46393  etransclem35  46715  hspmbllem2  47073  smflimlem2  47218  smflimlem4  47220  iccpartgt  47899  prproropf1olem4  47978  sfprmdvdsmersenne  48078  gricushgr  48405  2zlidl  48728  ply1mulgsumlem2  48875  nn0sumshdiglemA  49107  imaf1co  49642  uppropd  49668  fuco21  49823  functhinclem4  49934  2arwcat  50087