Theorem ad4antr 730

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad5antr  732  ad5antlr  733  simp-4l  781  tfrlem1  8360  prdsval  17385  catass  17614  catpropd  17637  cidpropd  17638  subccocl  17779  funcco  17805  natpropd  17913  fucpropd  17914  initoeu2lem1  17948  prfval  18135  xpcpropd  18145  acsfiindd  18490  mhmmnd  18921  mhpmulcl  21623  scmatscm  21946  cpmatmcllem  22151  mptcoe1matfsupp  22235  mp2pm2mplem4  22242  chpdmatlem2  22272  chfacfisf  22287  chfacfisfcpmat  22288  neitr  22615  hauscmplem  22841  trcfilu  23730  cfilucfil  23999  restmetu  24010  metucn  24011  cnheibor  24402  dvlip2  25443  lgamucov  26471  tgifscgr  27688  iscgrglt  27694  tgbtwnconn1  27755  legtrd  27769  legtri3  27770  legso  27779  hlcgrex  27796  tglndim0  27809  tglinethru  27816  tglnpt2  27821  colline  27829  perpneq  27894  isperp2  27895  footexALT  27898  opphllem  27915  midex  27917  opphllem3  27929  opphllem5  27931  opphllem6  27932  opphl  27934  outpasch  27935  hlpasch  27936  lnopp2hpgb  27943  hpgerlem  27945  lmieu  27964  lnperpex  27983  trgcopy  27984  cgrahl  28007  acopy  28013  inaghl  28025  cgrg3col4  28033  f1otrg  28051  nbumgrvtx  28532  3cyclfrgr  29470  numclwlk2lem2f1o  29561  s3f1  32048  dfmgc2  32101  pwrssmgc  32105  mgcf1o  32108  omndmul2  32165  psgnfzto1stlem  32194  cycpmrn  32237  tocyccntz  32238  cycpmconjs  32250  isarchi3  32268  archirngz  32270  nsgqusf1olem1  32444  nsgqusf1olem2  32445  nsgqusf1olem3  32446  ghmqusker  32451  lmhmqusker  32453  rhmpreimaidl  32456  rhmqusker  32459  elrspunidl  32461  elrspunsn  32462  idlinsubrg  32464  rhmimaidl  32465  drngidl  32466  isprmidlc  32481  qsidomlem1  32486  qsidomlem2  32487  mxidlprm  32501  opprqusplusg  32513  opprqusmulr  32515  qsdrngi  32519  qsdrng  32521  dimkerim  32614  fedgmul  32618  extdg1id  32644  qtophaus  32711  zarclsint  32747  zarcmplem  32756  esumcst  32956  sigapildsys  33055  oms0  33191  omssubadd  33194  carsgclctunlem3  33214  eulerpartlemgvv  33270  signsply0  33457  signstfvneq0  33478  actfunsnf1o  33511  reprsuc  33522  reprinfz1  33529  breprexplema  33537  breprexplemc  33539  hgt750lemb  33563  cvmlift3lem2  34206  satfdmlem  34254  nn0prpwlem  35075  lindsenlbs  36351  matunitlindflem1  36352  mblfinlem3  36395  mblfinlem4  36396  itg2addnclem2  36408  itg2gt0cn  36411  ftc1cnnc  36428  ftc1anc  36437  sstotbnd2  36511  lcfl8  40242  aks4d1p8  40821  fldhmf1  40824  aks6d1c2p2  40826  fsuppind  41015  prjspersym  41195  pell1234qrdich  41434  pell14qrdich  41442  pell1qrgap  41447  pellfundex  41459  omabs2  41917  cvgdvgrat  42907  infleinflem2  43918  xrralrecnnle  43930  climrec  44156  climsuse  44161  limcrecl  44182  limsupubuz  44266  limsupgtlem  44330  xlimliminflimsup  44415  fperdvper  44472  dvnprodlem2  44500  etransclem35  44822  hspmbllem2  45180  smflimlem2  45325  smflimlem4  45327  iccpartgt  45931  prproropf1olem4  46010  sfprmdvdsmersenne  46107  isomushgr  46330  isomuspgrlem1  46331  isomuspgrlem2d  46335  2zlidl  46544  mndpsuppss  46759  ply1mulgsumlem2  46780  nn0sumshdiglemA  47017  functhinclem4  47376