Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-5r Structured version   Visualization version   GIF version

Theorem simp-5r 826
 Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-5r ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simp-5r
StepHypRef Expression
1 simp-4r 824 . 2 (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
21adantr 480 1 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  simp-6r  828  catcocl  16393  catass  16394  monpropd  16444  subccocl  16552  funcco  16578  funcpropd  16607  mhmmnd  17584  pm2mpmhmlem2  20672  neitr  21032  restutopopn  22089  ustuqtop4  22095  utopreg  22103  cfilucfil  22411  psmetutop  22419  dyadmax  23412  tgifscgr  25448  tgcgrxfr  25458  tgbtwnconn1lem3  25514  tgbtwnconn1  25515  legov  25525  legtrd  25529  legso  25539  miriso  25610  perpneq  25654  footex  25658  colperpex  25670  opphllem  25672  midex  25674  opphl  25691  lnopp2hpgb  25700  trgcopyeu  25743  dfcgra2  25766  inaghl  25776  f1otrg  25796  clwlksfclwwlk  27049  2sqmo  29777  omndmul2  29840  psgnfzto1stlem  29978  qtophaus  30031  locfinreflem  30035  cmpcref  30045  pstmxmet  30068  lmxrge0  30126  esumcst  30253  omssubadd  30490  signstfvneq0  30777  afsval  30877  matunitlindflem1  33535  heicant  33574  sstotbnd2  33703  eldioph2b  37643  diophren  37694  pell1234qrdich  37742  iunconnlem2  39485  limcrecl  40179  limclner  40201  icccncfext  40418  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweidlem60  40595  fourierdlem51  40692  fourierdlem77  40718  fourierdlem103  40744  fourierdlem104  40745  smfaddlem1  41292  smfmullem3  41321
 Copyright terms: Public domain W3C validator