MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-6l Unicode version

Theorem simp-6l 771
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-6l

Proof of Theorem simp-6l
StepHypRef Expression
1 simp-5l 769 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  simp-7l  773  ghmcmn  16840  ustuqtop2  20745  ustuqtop4  20747  cnheibor  21455  miriso  24050  f1otrg  24174  txomap  27837  pstmxmet  27876  signstfvneq0  28529  limcleqr  31650  0ellimcdiv  31655  limclner  31657  fourierdlem51  31940  iunconlem2  33735
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 185  df-an 371
  Copyright terms: Public domain W3C validator