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  8376  prdsval  17401  catass  17630  catpropd  17653  cidpropd  17654  subccocl  17795  funcco  17821  natpropd  17929  fucpropd  17930  initoeu2lem1  17964  prfval  18151  xpcpropd  18161  acsfiindd  18506  mhmmnd  18947  mhpmulcl  21692  scmatscm  22015  cpmatmcllem  22220  mptcoe1matfsupp  22304  mp2pm2mplem4  22311  chpdmatlem2  22341  chfacfisf  22356  chfacfisfcpmat  22357  neitr  22684  hauscmplem  22910  trcfilu  23799  cfilucfil  24068  restmetu  24079  metucn  24080  cnheibor  24471  dvlip2  25512  lgamucov  26542  tgifscgr  27759  iscgrglt  27765  tgbtwnconn1  27826  legtrd  27840  legtri3  27841  legso  27850  hlcgrex  27867  tglndim0  27880  tglinethru  27887  tglnpt2  27892  colline  27900  perpneq  27965  isperp2  27966  footexALT  27969  opphllem  27986  midex  27988  opphllem3  28000  opphllem5  28002  opphllem6  28003  opphl  28005  outpasch  28006  hlpasch  28007  lnopp2hpgb  28014  hpgerlem  28016  lmieu  28035  lnperpex  28054  trgcopy  28055  cgrahl  28078  acopy  28084  inaghl  28096  cgrg3col4  28104  f1otrg  28122  nbumgrvtx  28603  3cyclfrgr  29541  numclwlk2lem2f1o  29632  s3f1  32113  dfmgc2  32166  pwrssmgc  32170  mgcf1o  32173  omndmul2  32230  psgnfzto1stlem  32259  cycpmrn  32302  tocyccntz  32303  cycpmconjs  32315  isarchi3  32333  archirngz  32335  nsgqusf1olem1  32524  nsgqusf1olem2  32525  nsgqusf1olem3  32526  ghmquskerlem3  32531  ghmqusker  32532  lmhmqusker  32534  rhmpreimaidl  32537  rhmquskerlem  32543  elrspunidl  32546  elrspunsn  32547  idlinsubrg  32549  rhmimaidl  32550  drngidl  32551  isprmidlc  32566  qsidomlem1  32571  qsidomlem2  32572  mxidlprm  32586  mxidlirredi  32587  mxidlirred  32588  opprqusplusg  32603  opprqusmulr  32605  qsdrngi  32609  qsdrng  32611  dimkerim  32712  fedgmul  32716  extdg1id  32742  minplyirred  32770  qtophaus  32816  zarclsint  32852  zarcmplem  32861  esumcst  33061  sigapildsys  33160  oms0  33296  omssubadd  33299  carsgclctunlem3  33319  eulerpartlemgvv  33375  signsply0  33562  signstfvneq0  33583  actfunsnf1o  33616  reprsuc  33627  reprinfz1  33634  breprexplema  33642  breprexplemc  33644  hgt750lemb  33668  cvmlift3lem2  34311  satfdmlem  34359  nn0prpwlem  35207  lindsenlbs  36483  matunitlindflem1  36484  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem2  36540  itg2gt0cn  36543  ftc1cnnc  36560  ftc1anc  36569  sstotbnd2  36642  lcfl8  40373  aks4d1p8  40952  fldhmf1  40955  aks6d1c2p2  40957  fsuppind  41162  prjspersym  41349  pell1234qrdich  41599  pell14qrdich  41607  pell1qrgap  41612  pellfundex  41624  omabs2  42082  cvgdvgrat  43072  infleinflem2  44081  xrralrecnnle  44093  climrec  44319  climsuse  44324  limcrecl  44345  limsupubuz  44429  limsupgtlem  44493  xlimliminflimsup  44578  fperdvper  44635  dvnprodlem2  44663  etransclem35  44985  hspmbllem2  45343  smflimlem2  45488  smflimlem4  45490  iccpartgt  46095  prproropf1olem4  46174  sfprmdvdsmersenne  46271  isomushgr  46494  isomuspgrlem1  46495  isomuspgrlem2d  46499  2zlidl  46832  mndpsuppss  47047  ply1mulgsumlem2  47068  nn0sumshdiglemA  47305  functhinclem4  47664