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

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

Proof of Theorem simpl1r
StepHypRef Expression
1 simp1r 1079 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
21adantr 480 1 ((((𝜑𝜓) ∧ 𝜒𝜃) ∧ 𝜏) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  soisores  6477  tfisi  6950  omopth2  7551  swrdsbslen  13300  swrdspsleq  13301  repswswrd  13382  ramub1lem1  15568  efgsfo  17975  lbspss  18903  maducoeval2  20265  madurid  20269  decpmatmullem  20395  mp2pm2mplem4  20433  llyrest  21098  ptbasin  21190  basqtop  21324  ustuqtop1  21855  mulcxp  24231  br8d  28802  isarchi2  29070  archiabllem2c  29080  cvmlift2lem10  30548  5segofs  31283  btwnconn1lem13  31376  2llnjaN  33870  paddasslem12  34135  lhp2lt  34305  lhpexle2lem  34313  lhpmcvr3  34329  lhpat3  34350  trlval3  34492  cdleme17b  34592  cdlemefr27cl  34709  cdlemg11b  34948  tendococl  35078  cdlemj3  35129  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk53b  35262  cdlemk35u  35270  cdlemm10N  35425  dihopelvalcpre  35555  dihord6apre  35563  dihord5b  35566  dihglblem5apreN  35598  dihglblem2N  35601  dihmeetlem6  35616  dihmeetlem18N  35631  dvh3dim2  35755  dvh3dim3N  35756  jm2.25lem1  36583  limcleqr  38711  icccncfext  38773  fourierdlem87  39086  sge0seq  39339
 Copyright terms: Public domain W3C validator