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

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

Proof of Theorem simp1lr
StepHypRef Expression
1 simplr 766 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant1 1132 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086
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 206  df-an 397  df-3an 1088
This theorem is referenced by:  lspsolvlem  20404  dmatcrng  21651  scmatcrng  21670  1marepvsma1  21732  mdetunilem7  21767  mat2pmatghm  21879  pmatcollpwscmatlem2  21939  mp2pm2mplem4  21958  ax5seg  27306  measinblem  32188  btwnconn1lem13  34401  athgt  37470  llnle  37532  lplnle  37554  lhpexle1  38022  lhpat3  38060  tendoicl  38810  cdlemk55b  38974  pellex  40657  ssfiunibd  42848  mullimc  43157  mullimcf  43164  icccncfext  43428  etransclem32  43807
  Copyright terms: Public domain W3C validator