Theorem ad4antr 728

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  ad5antr  730  ad5antlr  731  simp-4l  779  tfrlem1  8378  prdsval  17405  catass  17634  catpropd  17657  cidpropd  17658  subccocl  17799  funcco  17825  natpropd  17933  fucpropd  17934  initoeu2lem1  17968  prfval  18155  xpcpropd  18165  acsfiindd  18510  mhmmnd  18983  mhpmulcl  21911  scmatscm  22235  cpmatmcllem  22440  mptcoe1matfsupp  22524  mp2pm2mplem4  22531  chpdmatlem2  22561  chfacfisf  22576  chfacfisfcpmat  22577  neitr  22904  hauscmplem  23130  trcfilu  24019  cfilucfil  24288  restmetu  24299  metucn  24300  cnheibor  24701  dvlip2  25747  lgamucov  26778  tgifscgr  28026  iscgrglt  28032  tgbtwnconn1  28093  legtrd  28107  legtri3  28108  legso  28117  hlcgrex  28134  tglndim0  28147  tglinethru  28154  tglnpt2  28159  colline  28167  perpneq  28232  isperp2  28233  footexALT  28236  opphllem  28253  midex  28255  opphllem3  28267  opphllem5  28269  opphllem6  28270  opphl  28272  outpasch  28273  hlpasch  28274  lnopp2hpgb  28281  hpgerlem  28283  lmieu  28302  lnperpex  28321  trgcopy  28322  cgrahl  28345  acopy  28351  inaghl  28363  cgrg3col4  28371  f1otrg  28389  nbumgrvtx  28870  3cyclfrgr  29808  numclwlk2lem2f1o  29899  s3f1  32380  dfmgc2  32433  pwrssmgc  32437  mgcf1o  32440  omndmul2  32500  psgnfzto1stlem  32529  cycpmrn  32572  tocyccntz  32573  cycpmconjs  32585  isarchi3  32603  archirngz  32605  nsgqusf1olem1  32798  nsgqusf1olem2  32799  nsgqusf1olem3  32800  ghmquskerlem3  32805  ghmqusker  32806  lmhmqusker  32808  rhmpreimaidl  32811  rhmquskerlem  32817  elrspunidl  32820  elrspunsn  32821  idlinsubrg  32823  rhmimaidl  32824  drngidl  32825  isprmidlc  32840  qsidomlem1  32845  qsidomlem2  32846  mxidlprm  32860  mxidlirredi  32861  mxidlirred  32862  opprqusplusg  32877  opprqusmulr  32879  qsdrngi  32883  qsdrng  32885  dimkerim  33000  fedgmul  33004  extdg1id  33030  evls1fldgencl  33033  minplyirred  33059  qtophaus  33114  zarclsint  33150  zarcmplem  33159  esumcst  33359  sigapildsys  33458  oms0  33594  omssubadd  33597  carsgclctunlem3  33617  eulerpartlemgvv  33673  signsply0  33860  signstfvneq0  33881  actfunsnf1o  33914  reprsuc  33925  reprinfz1  33932  breprexplema  33940  breprexplemc  33942  hgt750lemb  33966  cvmlift3lem2  34609  satfdmlem  34657  nn0prpwlem  35510  lindsenlbs  36786  matunitlindflem1  36787  mblfinlem3  36830  mblfinlem4  36831  itg2addnclem2  36843  itg2gt0cn  36846  ftc1cnnc  36863  ftc1anc  36872  sstotbnd2  36945  lcfl8  40676  aks4d1p8  41258  fldhmf1  41261  aks6d1c2p2  41263  fsuppind  41464  prjspersym  41651  pell1234qrdich  41901  pell14qrdich  41909  pell1qrgap  41914  pellfundex  41926  omabs2  42384  cvgdvgrat  43374  infleinflem2  44379  xrralrecnnle  44391  climrec  44617  climsuse  44622  limcrecl  44643  limsupubuz  44727  limsupgtlem  44791  xlimliminflimsup  44876  fperdvper  44933  dvnprodlem2  44961  etransclem35  45283  hspmbllem2  45641  smflimlem2  45786  smflimlem4  45788  iccpartgt  46393  prproropf1olem4  46472  sfprmdvdsmersenne  46569  isomushgr  46792  isomuspgrlem1  46793  isomuspgrlem2d  46797  2zlidl  46920  mndpsuppss  47135  ply1mulgsumlem2  47155  nn0sumshdiglemA  47392  functhinclem4  47751