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  8303  prdsval  17363  catass  17596  catpropd  17619  cidpropd  17620  subccocl  17756  funcco  17782  natpropd  17890  fucpropd  17891  initoeu2lem1  17925  prfval  18109  xpcpropd  18118  acsfiindd  18463  chnind  18531  chnso  18534  mndpsuppss  18677  mhmmnd  18981  ghmqusnsg  19198  ghmquskerlem3  19202  ghmqusker  19203  omndmul2  20049  rhmpreimaidl  21218  rhmqusnsg  21226  mhpmulcl  22067  psdmul  22084  scmatscm  22431  cpmatmcllem  22636  mptcoe1matfsupp  22720  mp2pm2mplem4  22727  chpdmatlem2  22757  chfacfisf  22772  chfacfisfcpmat  22773  neitr  23098  hauscmplem  23324  trcfilu  24211  cfilucfil  24477  restmetu  24488  metucn  24489  cnheibor  24884  dvlip2  25930  lgamucov  26978  tgifscgr  28489  iscgrglt  28495  tgbtwnconn1  28556  legtrd  28570  legtri3  28571  legso  28580  hlcgrex  28597  tglndim0  28610  tglinethru  28617  tglnpt2  28622  colline  28630  perpneq  28695  isperp2  28696  footexALT  28699  opphllem  28716  midex  28718  opphllem3  28730  opphllem5  28732  opphllem6  28733  opphl  28735  outpasch  28736  hlpasch  28737  lnopp2hpgb  28744  hpgerlem  28746  lmieu  28765  lnperpex  28784  trgcopy  28785  cgrahl  28808  acopy  28814  inaghl  28826  cgrg3col4  28834  f1otrg  28852  nbumgrvtx  29328  3cyclfrgr  30272  numclwlk2lem2f1o  30363  s3f1  32937  ccatws1f1o  32941  dfmgc2  32986  pwrssmgc  32990  mgcf1o  32993  mndlrinvb  33015  gsumwun  33054  psgnfzto1stlem  33078  cycpmrn  33121  tocyccntz  33122  cycpmconjs  33134  isarchi3  33165  archirngz  33167  elrgspnlem2  33219  elrgspnlem4  33221  elrgspnsubrunlem2  33224  erler  33241  rlocaddval  33244  rlocmulval  33245  rloccring  33246  rloc1r  33248  fracfld  33283  nsgqusf1olem1  33387  nsgqusf1olem2  33388  nsgqusf1olem3  33389  lmhmqusker  33391  rhmquskerlem  33399  elrspunidl  33402  elrspunsn  33403  idlinsubrg  33405  rhmimaidl  33406  drngidl  33407  isprmidlc  33421  qsidomlem1  33426  qsidomlem2  33427  ssdifidlprm  33432  mxidlprm  33444  mxidlirredi  33445  mxidlirred  33446  drngmxidlr  33452  opprqusplusg  33463  opprqusmulr  33465  qsdrngi  33469  qsdrng  33471  rsprprmprmidlb  33497  rprmirred  33505  rprmirredb  33506  rprmdvdsprod  33508  1arithidom  33511  pidufd  33517  1arithufdlem2  33519  1arithufdlem3  33520  1arithufdlem4  33521  dfufd2lem  33523  mplmulmvr  33592  mplvrpmrhm  33597  esplyfv  33612  esplyind  33615  dimkerim  33663  fedgmul  33667  extdg1id  33702  evls1fldgencl  33706  fldextrspunlsplem  33709  fldextrspunlsp  33710  extdgfialglem1  33728  extdgfialg  33730  minplyirred  33747  constrextdg2lem  33784  constrfiss  33787  cos9thpiminplylem2  33819  qtophaus  33872  zarclsint  33908  zarcmplem  33917  esumcst  34099  sigapildsys  34198  oms0  34333  omssubadd  34336  carsgclctunlem3  34356  eulerpartlemgvv  34412  signsply0  34587  signstfvneq0  34608  actfunsnf1o  34640  reprsuc  34651  reprinfz1  34658  breprexplema  34666  breprexplemc  34668  hgt750lemb  34692  cvmlift3lem2  35387  satfdmlem  35435  nn0prpwlem  36389  lindsenlbs  37678  matunitlindflem1  37679  mblfinlem3  37722  mblfinlem4  37723  itg2addnclem2  37735  itg2gt0cn  37738  ftc1cnnc  37755  ftc1anc  37764  sstotbnd2  37837  lcfl8  41624  aks4d1p8  42203  fldhmf1  42206  mndmolinv  42211  primrootsunit1  42213  primrootscoprmpow  42215  primrootspoweq0  42222  aks6d1c2p2  42235  aks6d1c2lem4  42243  aks6d1c6lem3  42288  aks6d1c7  42300  unitscyglem2  42312  aks5  42320  fiabv  42657  fsuppind  42711  prjspersym  42728  pell1234qrdich  42981  pell14qrdich  42989  pell1qrgap  42994  pellfundex  43006  omabs2  43452  cvgdvgrat  44433  infleinflem2  45496  xrralrecnnle  45508  climrec  45730  climsuse  45735  limcrecl  45756  limsupubuz  45838  limsupgtlem  45902  xlimliminflimsup  45987  fperdvper  46044  dvnprodlem2  46072  etransclem35  46394  hspmbllem2  46752  smflimlem2  46897  smflimlem4  46899  iccpartgt  47554  prproropf1olem4  47633  sfprmdvdsmersenne  47730  gricushgr  48044  2zlidl  48367  ply1mulgsumlem2  48515  nn0sumshdiglemA  48747  imaf1co  49283  uppropd  49309  fuco21  49464  functhinclem4  49575  2arwcat  49728