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 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad3antrrr 729	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  733  ad5antlr  734  simp-4l  782  tfrlem1  8432  prdsval  17515  catass  17744  catpropd  17767  cidpropd  17768  subccocl  17909  funcco  17935  natpropd  18046  fucpropd  18047  initoeu2lem1  18081  prfval  18268  xpcpropd  18278  acsfiindd  18623  mhmmnd  19104  ghmqusnsg  19322  ghmquskerlem3  19326  ghmqusker  19327  rhmpreimaidl  21310  rhmqusnsg  21318  mhpmulcl  22176  psdmul  22193  scmatscm  22540  cpmatmcllem  22745  mptcoe1matfsupp  22829  mp2pm2mplem4  22836  chpdmatlem2  22866  chfacfisf  22881  chfacfisfcpmat  22882  neitr  23209  hauscmplem  23435  trcfilu  24324  cfilucfil  24593  restmetu  24604  metucn  24605  cnheibor  25006  dvlip2  26054  lgamucov  27099  tgifscgr  28534  iscgrglt  28540  tgbtwnconn1  28601  legtrd  28615  legtri3  28616  legso  28625  hlcgrex  28642  tglndim0  28655  tglinethru  28662  tglnpt2  28667  colline  28675  perpneq  28740  isperp2  28741  footexALT  28744  opphllem  28761  midex  28763  opphllem3  28775  opphllem5  28777  opphllem6  28778  opphl  28780  outpasch  28781  hlpasch  28782  lnopp2hpgb  28789  hpgerlem  28791  lmieu  28810  lnperpex  28829  trgcopy  28830  cgrahl  28853  acopy  28859  inaghl  28871  cgrg3col4  28879  f1otrg  28897  nbumgrvtx  29381  3cyclfrgr  30320  numclwlk2lem2f1o  30411  s3f1  32913  ccatws1f1o  32918  dfmgc2  32969  pwrssmgc  32973  mgcf1o  32976  chnind  32983  chnso  32986  mndlrinvb  33011  omndmul2  33062  psgnfzto1stlem  33093  cycpmrn  33136  tocyccntz  33137  cycpmconjs  33149  isarchi3  33167  archirngz  33169  erler  33237  rlocaddval  33240  rlocmulval  33241  rloccring  33242  rloc1r  33244  fracfld  33275  nsgqusf1olem1  33406  nsgqusf1olem2  33407  nsgqusf1olem3  33408  lmhmqusker  33410  rhmquskerlem  33418  elrspunidl  33421  elrspunsn  33422  idlinsubrg  33424  rhmimaidl  33425  drngidl  33426  isprmidlc  33440  qsidomlem1  33445  qsidomlem2  33446  ssdifidlprm  33451  mxidlprm  33463  mxidlirredi  33464  mxidlirred  33465  drngmxidlr  33471  opprqusplusg  33482  opprqusmulr  33484  qsdrngi  33488  qsdrng  33490  rsprprmprmidlb  33516  rprmirred  33524  rprmirredb  33525  rprmdvdsprod  33527  1arithidom  33530  pidufd  33536  1arithufdlem2  33538  1arithufdlem3  33539  1arithufdlem4  33540  dfufd2lem  33542  dimkerim  33640  fedgmul  33644  extdg1id  33676  evls1fldgencl  33680  minplyirred  33704  qtophaus  33782  zarclsint  33818  zarcmplem  33827  esumcst  34027  sigapildsys  34126  oms0  34262  omssubadd  34265  carsgclctunlem3  34285  eulerpartlemgvv  34341  signsply0  34528  signstfvneq0  34549  actfunsnf1o  34581  reprsuc  34592  reprinfz1  34599  breprexplema  34607  breprexplemc  34609  hgt750lemb  34633  cvmlift3lem2  35288  satfdmlem  35336  nn0prpwlem  36288  lindsenlbs  37575  matunitlindflem1  37576  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem2  37632  itg2gt0cn  37635  ftc1cnnc  37652  ftc1anc  37661  sstotbnd2  37734  lcfl8  41459  aks4d1p8  42044  fldhmf1  42047  mndmolinv  42052  primrootsunit1  42054  primrootscoprmpow  42056  primrootspoweq0  42063  aks6d1c2p2  42076  aks6d1c2lem4  42084  aks6d1c6lem3  42129  aks6d1c7  42141  unitscyglem2  42153  aks5  42161  fiabv  42491  fsuppind  42545  prjspersym  42562  pell1234qrdich  42817  pell14qrdich  42825  pell1qrgap  42830  pellfundex  42842  omabs2  43294  cvgdvgrat  44282  infleinflem2  45286  xrralrecnnle  45298  climrec  45524  climsuse  45529  limcrecl  45550  limsupubuz  45634  limsupgtlem  45698  xlimliminflimsup  45783  fperdvper  45840  dvnprodlem2  45868  etransclem35  46190  hspmbllem2  46548  smflimlem2  46693  smflimlem4  46695  iccpartgt  47301  prproropf1olem4  47380  sfprmdvdsmersenne  47477  gricushgr  47770  2zlidl  47963  mndpsuppss  48096  ply1mulgsumlem2  48116  nn0sumshdiglemA  48353  functhinclem4  48711