ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sseq12d GIF version

Theorem sseq12d 3178
Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
Hypotheses
Ref Expression
sseq1d.1 (𝜑𝐴 = 𝐵)
sseq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
sseq12d (𝜑 → (𝐴𝐶𝐵𝐷))

Proof of Theorem sseq12d
StepHypRef Expression
1 sseq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21sseq1d 3176 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
3 sseq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43sseq2d 3177 . 2 (𝜑 → (𝐵𝐶𝐵𝐷))
52, 4bitrd 187 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1348  wss 3121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134
This theorem is referenced by:  3sstr3d  3191  3sstr4d  3192  ssdifeq0  3497  relcnvtr  5130  rdgisucinc  6364  oawordriexmid  6449  nnaword  6490  nnawordi  6494  sbthlem2  6935  isbth  6944  nninff  7099  infnninf  7100  infnninfOLD  7101  nnnninf  7102  nnnninfeq  7104  nnnninfeq2  7105  nninfwlpoimlemg  7151  ennnfonelemkh  12367  ennnfonelemrnh  12371  isstruct2im  12426  isstruct2r  12427  ressid2  12477  ressval2  12478  basis1  12839  baspartn  12842  eltg  12846  metss  13288  0nninf  14037  nnsf  14038  peano4nninf  14039  nninfalllem1  14041  nninfself  14046
  Copyright terms: Public domain W3C validator