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

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

Proof of Theorem simpl1r
StepHypRef Expression
1 simp1r 1084 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
21adantr 481 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:  soisores  6537  tfisi  7012  omopth2  7616  swrdsbslen  13394  swrdspsleq  13395  repswswrd  13476  ramub1lem1  15665  efgsfo  18084  lbspss  19014  maducoeval2  20378  madurid  20382  decpmatmullem  20508  mp2pm2mplem4  20546  llyrest  21211  ptbasin  21303  basqtop  21437  ustuqtop1  21968  mulcxp  24348  br8d  29288  isarchi2  29548  archiabllem2c  29558  cvmlift2lem10  31037  5segofs  31790  btwnconn1lem13  31883  2llnjaN  34367  paddasslem12  34632  lhp2lt  34802  lhpexle2lem  34810  lhpmcvr3  34826  lhpat3  34847  trlval3  34989  cdleme17b  35089  cdlemefr27cl  35206  cdlemg11b  35445  tendococl  35575  cdlemj3  35626  cdlemk35s-id  35741  cdlemk39s-id  35743  cdlemk53b  35759  cdlemk35u  35767  cdlemm10N  35922  dihopelvalcpre  36052  dihord6apre  36060  dihord5b  36063  dihglblem5apreN  36095  dihglblem2N  36098  dihmeetlem6  36113  dihmeetlem18N  36128  dvh3dim2  36252  dvh3dim3N  36253  jm2.25lem1  37080  limcleqr  39308  icccncfext  39431  fourierdlem87  39743  sge0seq  39996  smflimsuplem7  40365
  Copyright terms: Public domain W3C validator