MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1lr Structured version   Visualization version   GIF version

Theorem simp1lr 1275
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp1lr ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜓)

Proof of Theorem simp1lr
StepHypRef Expression
1 simplr 759 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant1 1124 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071
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 199  df-an 387  df-3an 1073
This theorem is referenced by:  lspsolvlem  19538  dmatcrng  20713  scmatcrng  20732  1marepvsma1  20794  mdetunilem7  20829  mat2pmatghm  20942  pmatcollpwscmatlem2  21002  mp2pm2mplem4  21021  ax5seg  26287  measinblem  30881  btwnconn1lem13  32795  athgt  35612  llnle  35674  lplnle  35696  lhpexle1  36164  lhpat3  36202  tendoicl  36952  cdlemk55b  37116  pellex  38363  ssfiunibd  40436  mullimc  40760  mullimcf  40767  icccncfext  41032  etransclem32  41414
  Copyright terms: Public domain W3C validator