Theorem simp-5r 784

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

Assertion

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

Proof of Theorem simp-5r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad5antlr 733	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:  catcocl  16958  catass  16959  monpropd  17009  subccocl  17117  funcco  17143  funcpropd  17172  mhmmnd  18223  pm2mpmhmlem2  21429  neitr  21790  restutopopn  22849  ustuqtop4  22855  utopreg  22863  cfilucfil  23171  psmetutop  23179  dyadmax  24201  2sqmo  26015  tgifscgr  26296  tgcgrxfr  26306  tgbtwnconn1lem3  26362  tgbtwnconn1  26363  legov  26373  legtrd  26377  legso  26387  miriso  26458  perpneq  26502  footexALT  26506  footex  26509  colperpex  26521  opphllem  26523  midex  26525  opphl  26542  lnopp2hpgb  26551  trgcopyeu  26594  dfcgra2  26618  inaghl  26633  f1otrg  26659  nn0xmulclb  30498  omndmul2  30715  psgnfzto1stlem  30744  cyc3genpm  30796  mxidlprm  30979  ssmxidl  30981  lbsdiflsp0  31024  qtophaus  31102  locfinreflem  31106  cmpcref  31116  pstmxmet  31139  lmxrge0  31197  esumcst  31324  omssubadd  31560  signstfvneq0  31844  afsval  31944  matunitlindflem1  34890  heicant  34929  sstotbnd2  35054  dffltz  39278  eldioph2b  39367  diophren  39417  pell1234qrdich  39465  iunconnlem2  41276  limcrecl  41917  limclner  41939  icccncfext  42177  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  stoweidlem60  42352  fourierdlem51  42449  fourierdlem77  42475  fourierdlem103  42501  fourierdlem104  42502  smfaddlem1  43046  smfmullem3  43075