Theorem ad4antr 729

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 727	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  731  ad5antlr  732  simp-4l  780  tfrlem1  8207  prdsval  17166  catass  17395  catpropd  17418  cidpropd  17419  subccocl  17560  funcco  17586  natpropd  17694  fucpropd  17695  initoeu2lem1  17729  prfval  17916  xpcpropd  17926  acsfiindd  18271  mhmmnd  18697  mhpmulcl  21339  scmatscm  21662  cpmatmcllem  21867  mptcoe1matfsupp  21951  mp2pm2mplem4  21958  chpdmatlem2  21988  chfacfisf  22003  chfacfisfcpmat  22004  neitr  22331  hauscmplem  22557  trcfilu  23446  cfilucfil  23715  restmetu  23726  metucn  23727  cnheibor  24118  dvlip2  25159  lgamucov  26187  tgifscgr  26869  iscgrglt  26875  tgbtwnconn1  26936  legtrd  26950  legtri3  26951  legso  26960  hlcgrex  26977  tglndim0  26990  tglinethru  26997  tglnpt2  27002  colline  27010  perpneq  27075  isperp2  27076  footexALT  27079  opphllem  27096  midex  27098  opphllem3  27110  opphllem5  27112  opphllem6  27113  opphl  27115  outpasch  27116  hlpasch  27117  lnopp2hpgb  27124  hpgerlem  27126  lmieu  27145  lnperpex  27164  trgcopy  27165  cgrahl  27188  acopy  27194  inaghl  27206  cgrg3col4  27214  f1otrg  27232  nbumgrvtx  27713  3cyclfrgr  28652  numclwlk2lem2f1o  28743  s3f1  31221  dfmgc2  31274  pwrssmgc  31278  mgcf1o  31281  omndmul2  31338  psgnfzto1stlem  31367  cycpmrn  31410  tocyccntz  31411  cycpmconjs  31423  isarchi3  31441  archirngz  31443  nsgqusf1olem1  31598  nsgqusf1olem2  31599  nsgqusf1olem3  31600  rhmpreimaidl  31603  elrspunidl  31606  idlinsubrg  31608  rhmimaidl  31609  isprmidlc  31623  qsidomlem1  31628  qsidomlem2  31629  mxidlprm  31640  dimkerim  31708  fedgmul  31712  extdg1id  31738  qtophaus  31786  zarclsint  31822  zarcmplem  31831  esumcst  32031  sigapildsys  32130  oms0  32264  omssubadd  32267  carsgclctunlem3  32287  eulerpartlemgvv  32343  signsply0  32530  signstfvneq0  32551  actfunsnf1o  32584  reprsuc  32595  reprinfz1  32602  breprexplema  32610  breprexplemc  32612  hgt750lemb  32636  cvmlift3lem2  33282  satfdmlem  33330  nn0prpwlem  34511  lindsenlbs  35772  matunitlindflem1  35773  mblfinlem3  35816  mblfinlem4  35817  itg2addnclem2  35829  itg2gt0cn  35832  ftc1cnnc  35849  ftc1anc  35858  sstotbnd2  35932  lcfl8  39516  aks4d1p8  40095  fsuppind  40279  prjspersym  40446  pell1234qrdich  40683  pell14qrdich  40691  pell1qrgap  40696  pellfundex  40708  cvgdvgrat  41931  infleinflem2  42910  xrralrecnnle  42922  climrec  43144  climsuse  43149  limcrecl  43170  limsupubuz  43254  limsupgtlem  43318  xlimliminflimsup  43403  fperdvper  43460  dvnprodlem2  43488  etransclem35  43810  hspmbllem2  44165  smflimlem2  44307  smflimlem4  44309  iccpartgt  44879  prproropf1olem4  44958  sfprmdvdsmersenne  45055  isomushgr  45278  isomuspgrlem1  45279  isomuspgrlem2d  45283  2zlidl  45492  mndpsuppss  45707  ply1mulgsumlem2  45728  nn0sumshdiglemA  45965  functhinclem4  46325