Theorem simp-4r 782

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-4r	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 731	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fimaproj  7831  tfrlem1  8014  injresinj  13161  swrdccatin1  14089  reuccatpfxs1  14111  prdsval  16730  catcocl  16958  catass  16959  catpropd  16981  cidpropd  16982  monpropd  17009  subccocl  17117  funcco  17143  funcpropd  17172  fucpropd  17249  initoeu2lem1  17276  xpcpropd  17460  curf2ndf  17499  drsdirfi  17550  mhmmnd  18223  gsmsymgreqlem2  18561  dfod2  18693  ghmcmn  18954  psgndif  20748  dmatscmcl  21114  smatvscl  21135  cpmatmcllem  21328  pm2mpmhmlem2  21429  chfacfscmulgsum  21470  chfacfpmmulgsum  21474  neitr  21790  1stcrest  22063  dissnref  22138  dissnlocfin  22139  neitx  22217  tgqtop  22322  ptcmplem3  22664  trust  22840  utoptop  22845  restutopopn  22849  ustuqtop2  22853  ustuqtop4  22855  utop3cls  22862  met1stc  23133  prdsxmslem2  23141  metustexhalf  23168  cfilucfil  23171  metucn  23183  aannenlem1  24919  ulmuni  24982  lgamucov  25617  2sqmo  26015  pntpbnd  26166  pntlem3  26187  istrkgb  26243  tgbtwndiff  26294  tgifscgr  26296  iscgrglt  26302  tgbtwnconn1lem3  26362  tgbtwnconn1  26363  legov  26373  legtrd  26377  legtri3  26378  ltgseg  26384  legso  26387  tglinethru  26424  tglnpt2  26429  colline  26437  miriso  26458  midexlem  26480  perpneq  26502  isperp2  26503  footexALT  26506  footex  26509  midex  26525  opphllem3  26537  opphl  26542  hlpasch  26544  lnopp2hpgb  26551  lmieu  26572  trgcopyeu  26594  dfcgra2  26618  f1otrg  26659  axcontlem2  26753  2pthon3v  27724  fnpreimac  30418  fsumiunle  30547  ressprs  30644  omndmul2  30715  tocyccntz  30788  cyc3genpm  30796  cycpmconjs  30800  cyc3conja  30801  isarchi3  30818  isarchiofld  30892  imaslmod  30924  isprmidlc  30965  qsidomlem2  30968  mxidlprm  30979  ssmxidllem  30980  ssmxidl  30981  lbsdiflsp0  31024  dimkerim  31025  fedgmul  31029  txomap  31100  qtophaus  31102  pstmxmet  31139  sqsscirc1  31153  lmxrge0  31197  esumcst  31324  esumfsup  31331  esum2dlem  31353  esum2d  31354  esumiun  31355  ldsysgenld  31421  sigapildsys  31423  omssubadd  31560  signstfvneq0  31844  actfunsnf1o  31877  afsval  31944  noetalem3  33221  nn0prpwlem  33672  lindsenlbs  34889  matunitlindflem1  34890  matunitlindflem2  34891  mblfinlem3  34933  itg2addnclem  34945  sstotbnd2  35054  prdstotbnd  35074  lcfl8  38640  dffltz  39278  diophren  39417  rencldnfilem  39424  pellex  39439  pell1234qrdich  39465  pell1qrgap  39478  pellfundex  39490  iunconnlem2  41276  suplesup  41614  infleinflem2  41646  xrralrecnnle  41660  rexabslelem  41699  limcrecl  41917  limcleqr  41932  0ellimcdiv  41937  limclner  41939  limsupubuz  42001  limsupvaluz2  42026  supcnvlimsup  42028  climxrre  42038  xlimmnfvlem2  42121  xlimmnfv  42122  xlimpnfvlem2  42125  xlimpnfv  42126  icccncfext  42177  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  fourierdlem50  42448  fourierdlem51  42449  fourierdlem80  42478  fourierdlem87  42485  fourierdlem103  42501  fourierdlem104  42502  meaiuninc3v  42773  omef  42785  smflimlem2  43055  smflimlem4  43057  smfmullem3  43075