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

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

Proof of Theorem simp1lr
StepHypRef Expression
1 simplr 768 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant1 1130 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃𝜏) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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  df-3an 1086 This theorem is referenced by:  lspsolvlem  19907  dmatcrng  21104  scmatcrng  21123  1marepvsma1  21185  mdetunilem7  21220  mat2pmatghm  21331  pmatcollpwscmatlem2  21391  mp2pm2mplem4  21410  ax5seg  26728  measinblem  31504  btwnconn1lem13  33585  athgt  36662  llnle  36724  lplnle  36746  lhpexle1  37214  lhpat3  37252  tendoicl  38002  cdlemk55b  38166  pellex  39629  ssfiunibd  41804  mullimc  42121  mullimcf  42128  icccncfext  42392  etransclem32  42771
 Copyright terms: Public domain W3C validator