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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad5antr  734  ad5antlr  735  simp-4l  782  tfrlem1  8344  prdsval  17418  catass  17647  catpropd  17670  cidpropd  17671  subccocl  17807  funcco  17833  natpropd  17941  fucpropd  17942  initoeu2lem1  17976  prfval  18160  xpcpropd  18169  acsfiindd  18512  mndpsuppss  18692  mhmmnd  18996  ghmqusnsg  19214  ghmquskerlem3  19218  ghmqusker  19219  rhmpreimaidl  21187  rhmqusnsg  21195  mhpmulcl  22036  psdmul  22053  scmatscm  22400  cpmatmcllem  22605  mptcoe1matfsupp  22689  mp2pm2mplem4  22696  chpdmatlem2  22726  chfacfisf  22741  chfacfisfcpmat  22742  neitr  23067  hauscmplem  23293  trcfilu  24181  cfilucfil  24447  restmetu  24458  metucn  24459  cnheibor  24854  dvlip2  25900  lgamucov  26948  tgifscgr  28435  iscgrglt  28441  tgbtwnconn1  28502  legtrd  28516  legtri3  28517  legso  28526  hlcgrex  28543  tglndim0  28556  tglinethru  28563  tglnpt2  28568  colline  28576  perpneq  28641  isperp2  28642  footexALT  28645  opphllem  28662  midex  28664  opphllem3  28676  opphllem5  28678  opphllem6  28679  opphl  28681  outpasch  28682  hlpasch  28683  lnopp2hpgb  28690  hpgerlem  28692  lmieu  28711  lnperpex  28730  trgcopy  28731  cgrahl  28754  acopy  28760  inaghl  28772  cgrg3col4  28780  f1otrg  28798  nbumgrvtx  29273  3cyclfrgr  30217  numclwlk2lem2f1o  30308  s3f1  32868  ccatws1f1o  32873  dfmgc2  32922  pwrssmgc  32926  mgcf1o  32929  chnind  32937  chnso  32940  mndlrinvb  32966  gsumwun  33005  omndmul2  33026  psgnfzto1stlem  33057  cycpmrn  33100  tocyccntz  33101  cycpmconjs  33113  isarchi3  33141  archirngz  33143  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem2  33199  erler  33216  rlocaddval  33219  rlocmulval  33220  rloccring  33221  rloc1r  33223  fracfld  33258  nsgqusf1olem1  33384  nsgqusf1olem2  33385  nsgqusf1olem3  33386  lmhmqusker  33388  rhmquskerlem  33396  elrspunidl  33399  elrspunsn  33400  idlinsubrg  33402  rhmimaidl  33403  drngidl  33404  isprmidlc  33418  qsidomlem1  33423  qsidomlem2  33424  ssdifidlprm  33429  mxidlprm  33441  mxidlirredi  33442  mxidlirred  33443  drngmxidlr  33449  opprqusplusg  33460  opprqusmulr  33462  qsdrngi  33466  qsdrng  33468  rsprprmprmidlb  33494  rprmirred  33502  rprmirredb  33503  rprmdvdsprod  33505  1arithidom  33508  pidufd  33514  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  dimkerim  33623  fedgmul  33627  extdg1id  33661  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  minplyirred  33701  constrextdg2lem  33738  constrfiss  33741  cos9thpiminplylem2  33773  qtophaus  33826  zarclsint  33862  zarcmplem  33871  esumcst  34053  sigapildsys  34152  oms0  34288  omssubadd  34291  carsgclctunlem3  34311  eulerpartlemgvv  34367  signsply0  34542  signstfvneq0  34563  actfunsnf1o  34595  reprsuc  34606  reprinfz1  34613  breprexplema  34621  breprexplemc  34623  hgt750lemb  34647  cvmlift3lem2  35307  satfdmlem  35355  nn0prpwlem  36310  lindsenlbs  37609  matunitlindflem1  37610  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem2  37666  itg2gt0cn  37669  ftc1cnnc  37686  ftc1anc  37695  sstotbnd2  37768  lcfl8  41496  aks4d1p8  42075  fldhmf1  42078  mndmolinv  42083  primrootsunit1  42085  primrootscoprmpow  42087  primrootspoweq0  42094  aks6d1c2p2  42107  aks6d1c2lem4  42115  aks6d1c6lem3  42160  aks6d1c7  42172  unitscyglem2  42184  aks5  42192  fiabv  42524  fsuppind  42578  prjspersym  42595  pell1234qrdich  42849  pell14qrdich  42857  pell1qrgap  42862  pellfundex  42874  omabs2  43321  cvgdvgrat  44302  infleinflem2  45367  xrralrecnnle  45379  climrec  45601  climsuse  45606  limcrecl  45627  limsupubuz  45711  limsupgtlem  45775  xlimliminflimsup  45860  fperdvper  45917  dvnprodlem2  45945  etransclem35  46267  hspmbllem2  46625  smflimlem2  46770  smflimlem4  46772  iccpartgt  47428  prproropf1olem4  47507  sfprmdvdsmersenne  47604  gricushgr  47917  2zlidl  48228  ply1mulgsumlem2  48376  nn0sumshdiglemA  48608  imaf1co  49144  uppropd  49170  fuco21  49325  functhinclem4  49436  2arwcat  49589