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

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

Proof of Theorem simp1lr
StepHypRef Expression
1 simplr 791 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant1 1080 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  lspsolvlem  19123  dmatcrng  20289  scmatcrng  20308  1marepvsma1  20370  mdetunilem7  20405  mat2pmatghm  20516  pmatcollpwscmatlem2  20576  mp2pm2mplem4  20595  ax5seg  25799  clwwnisshclwwsn  26910  measinblem  30257  btwnconn1lem13  32181  athgt  34561  llnle  34623  lplnle  34645  lhpexle1  35113  lhpat3  35151  tendoicl  35903  cdlemk55b  36067  pellex  37218  ssfiunibd  39336  mullimc  39648  mullimcf  39655  icccncfext  39863  etransclem32  40246
  Copyright terms: Public domain W3C validator