Theorem ad4antr 732

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad5antr  734  ad5antlr  735  simp-4l  783  tfrlem1  8090  prdsval  16914  catass  17143  catpropd  17166  cidpropd  17167  subccocl  17305  funcco  17331  natpropd  17439  fucpropd  17440  initoeu2lem1  17474  prfval  17660  xpcpropd  17670  acsfiindd  18013  mhmmnd  18439  mhpmulcl  21043  scmatscm  21364  cpmatmcllem  21569  mptcoe1matfsupp  21653  mp2pm2mplem4  21660  chpdmatlem2  21690  chfacfisf  21705  chfacfisfcpmat  21706  neitr  22031  hauscmplem  22257  trcfilu  23145  cfilucfil  23411  restmetu  23422  metucn  23423  cnheibor  23806  dvlip2  24846  lgamucov  25874  tgifscgr  26553  iscgrglt  26559  tgbtwnconn1  26620  legtrd  26634  legtri3  26635  legso  26644  hlcgrex  26661  tglndim0  26674  tglinethru  26681  tglnpt2  26686  colline  26694  perpneq  26759  isperp2  26760  footexALT  26763  opphllem  26780  midex  26782  opphllem3  26794  opphllem5  26796  opphllem6  26797  opphl  26799  outpasch  26800  hlpasch  26801  lnopp2hpgb  26808  hpgerlem  26810  lmieu  26829  lnperpex  26848  trgcopy  26849  cgrahl  26872  acopy  26878  inaghl  26890  cgrg3col4  26898  f1otrg  26916  nbumgrvtx  27388  3cyclfrgr  28325  numclwlk2lem2f1o  28416  s3f1  30895  dfmgc2  30947  pwrssmgc  30951  mgcf1o  30954  omndmul2  31011  psgnfzto1stlem  31040  cycpmrn  31083  tocyccntz  31084  cycpmconjs  31096  isarchi3  31114  archirngz  31116  nsgqusf1olem1  31266  nsgqusf1olem2  31267  nsgqusf1olem3  31268  rhmpreimaidl  31271  elrspunidl  31274  idlinsubrg  31276  rhmimaidl  31277  isprmidlc  31291  qsidomlem1  31296  qsidomlem2  31297  mxidlprm  31308  dimkerim  31376  fedgmul  31380  extdg1id  31406  qtophaus  31454  zarclsint  31490  zarcmplem  31499  esumcst  31697  sigapildsys  31796  oms0  31930  omssubadd  31933  carsgclctunlem3  31953  eulerpartlemgvv  32009  signsply0  32196  signstfvneq0  32217  actfunsnf1o  32250  reprsuc  32261  reprinfz1  32268  breprexplema  32276  breprexplemc  32278  hgt750lemb  32302  cvmlift3lem2  32949  satfdmlem  32997  nn0prpwlem  34197  lindsenlbs  35458  matunitlindflem1  35459  mblfinlem3  35502  mblfinlem4  35503  itg2addnclem2  35515  itg2gt0cn  35518  ftc1cnnc  35535  ftc1anc  35544  sstotbnd2  35618  lcfl8  39202  fsuppind  39930  prjspersym  40095  pell1234qrdich  40327  pell14qrdich  40335  pell1qrgap  40340  pellfundex  40352  cvgdvgrat  41545  infleinflem2  42524  xrralrecnnle  42536  climrec  42762  climsuse  42767  limcrecl  42788  limsupubuz  42872  limsupgtlem  42936  xlimliminflimsup  43021  fperdvper  43078  dvnprodlem2  43106  etransclem35  43428  hspmbllem2  43783  smflimlem2  43922  smflimlem4  43924  iccpartgt  44495  prproropf1olem4  44574  sfprmdvdsmersenne  44671  isomushgr  44894  isomuspgrlem1  44895  isomuspgrlem2d  44899  2zlidl  45108  mndpsuppss  45323  ply1mulgsumlem2  45344  nn0sumshdiglemA  45581  functhinclem4  45941