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

Theorem simp-5r 785
 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
StepHypRef Expression
1 id 22 . 2 (𝜓𝜓)
21ad5antlr 734 1 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  catcocl  16956  catass  16957  monpropd  17007  subccocl  17115  funcco  17141  funcpropd  17170  mhmmnd  18221  pm2mpmhmlem2  21427  neitr  21788  restutopopn  22847  ustuqtop4  22853  utopreg  22861  cfilucfil  23169  psmetutop  23177  dyadmax  24205  2sqmo  26024  tgifscgr  26305  tgcgrxfr  26315  tgbtwnconn1lem3  26371  tgbtwnconn1  26372  legov  26382  legtrd  26386  legso  26396  miriso  26467  perpneq  26511  footexALT  26515  footex  26518  colperpex  26530  opphllem  26532  midex  26534  opphl  26551  lnopp2hpgb  26560  trgcopyeu  26603  dfcgra2  26627  inaghl  26642  f1otrg  26668  nn0xmulclb  30507  omndmul2  30745  psgnfzto1stlem  30774  cyc3genpm  30826  mxidlprm  31018  ssmxidl  31020  lbsdiflsp0  31082  qtophaus  31160  locfinreflem  31164  cmpcref  31174  pstmxmet  31197  lmxrge0  31252  esumcst  31379  omssubadd  31615  signstfvneq0  31899  afsval  31999  matunitlindflem1  34998  heicant  35037  sstotbnd2  35157  dffltz  39531  eldioph2b  39620  diophren  39670  pell1234qrdich  39718  iunconnlem2  41561  limcrecl  42197  limclner  42219  icccncfext  42455  ioodvbdlimc1lem2  42500  ioodvbdlimc2lem  42502  stoweidlem60  42628  fourierdlem51  42725  fourierdlem77  42751  fourierdlem103  42777  fourierdlem104  42778  smfaddlem1  43322  smfmullem3  43351
 Copyright terms: Public domain W3C validator