Theorem ad4antr 731

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 482	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad3antrrr 729	1 ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ad5antr  733  ad5antlr  734  simp-4l  782  tfrlem1  8373  prdsval  17398  catass  17627  catpropd  17650  cidpropd  17651  subccocl  17792  funcco  17818  natpropd  17926  fucpropd  17927  initoeu2lem1  17961  prfval  18148  xpcpropd  18158  acsfiindd  18503  mhmmnd  18942  mhpmulcl  21684  scmatscm  22007  cpmatmcllem  22212  mptcoe1matfsupp  22296  mp2pm2mplem4  22303  chpdmatlem2  22333  chfacfisf  22348  chfacfisfcpmat  22349  neitr  22676  hauscmplem  22902  trcfilu  23791  cfilucfil  24060  restmetu  24071  metucn  24072  cnheibor  24463  dvlip2  25504  lgamucov  26532  tgifscgr  27749  iscgrglt  27755  tgbtwnconn1  27816  legtrd  27830  legtri3  27831  legso  27840  hlcgrex  27857  tglndim0  27870  tglinethru  27877  tglnpt2  27882  colline  27890  perpneq  27955  isperp2  27956  footexALT  27959  opphllem  27976  midex  27978  opphllem3  27990  opphllem5  27992  opphllem6  27993  opphl  27995  outpasch  27996  hlpasch  27997  lnopp2hpgb  28004  hpgerlem  28006  lmieu  28025  lnperpex  28044  trgcopy  28045  cgrahl  28068  acopy  28074  inaghl  28086  cgrg3col4  28094  f1otrg  28112  nbumgrvtx  28593  3cyclfrgr  29531  numclwlk2lem2f1o  29622  s3f1  32101  dfmgc2  32154  pwrssmgc  32158  mgcf1o  32161  omndmul2  32218  psgnfzto1stlem  32247  cycpmrn  32290  tocyccntz  32291  cycpmconjs  32303  isarchi3  32321  archirngz  32323  nsgqusf1olem1  32513  nsgqusf1olem2  32514  nsgqusf1olem3  32515  ghmquskerlem3  32520  ghmqusker  32521  lmhmqusker  32523  rhmpreimaidl  32526  rhmquskerlem  32532  elrspunidl  32535  elrspunsn  32536  idlinsubrg  32538  rhmimaidl  32539  drngidl  32540  isprmidlc  32555  qsidomlem1  32560  qsidomlem2  32561  mxidlprm  32575  mxidlirredi  32576  mxidlirred  32577  opprqusplusg  32592  opprqusmulr  32594  qsdrngi  32598  qsdrng  32600  dimkerim  32701  fedgmul  32705  extdg1id  32731  minplyirred  32759  qtophaus  32805  zarclsint  32841  zarcmplem  32850  esumcst  33050  sigapildsys  33149  oms0  33285  omssubadd  33288  carsgclctunlem3  33308  eulerpartlemgvv  33364  signsply0  33551  signstfvneq0  33572  actfunsnf1o  33605  reprsuc  33616  reprinfz1  33623  breprexplema  33631  breprexplemc  33633  hgt750lemb  33657  cvmlift3lem2  34300  satfdmlem  34348  nn0prpwlem  35196  lindsenlbs  36472  matunitlindflem1  36473  mblfinlem3  36516  mblfinlem4  36517  itg2addnclem2  36529  itg2gt0cn  36532  ftc1cnnc  36549  ftc1anc  36558  sstotbnd2  36631  lcfl8  40362  aks4d1p8  40941  fldhmf1  40944  aks6d1c2p2  40946  fsuppind  41160  prjspersym  41346  pell1234qrdich  41585  pell14qrdich  41593  pell1qrgap  41598  pellfundex  41610  omabs2  42068  cvgdvgrat  43058  infleinflem2  44068  xrralrecnnle  44080  climrec  44306  climsuse  44311  limcrecl  44332  limsupubuz  44416  limsupgtlem  44480  xlimliminflimsup  44565  fperdvper  44622  dvnprodlem2  44650  etransclem35  44972  hspmbllem2  45330  smflimlem2  45475  smflimlem4  45477  iccpartgt  46082  prproropf1olem4  46161  sfprmdvdsmersenne  46258  isomushgr  46481  isomuspgrlem1  46482  isomuspgrlem2d  46486  2zlidl  46786  mndpsuppss  47001  ply1mulgsumlem2  47022  nn0sumshdiglemA  47259  functhinclem4  47618