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

Theorem sseqtrrdi 3228
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrrdi.1 (𝜑𝐴𝐵)
sseqtrrdi.2 𝐶 = 𝐵
Assertion
Ref Expression
sseqtrrdi (𝜑𝐴𝐶)

Proof of Theorem sseqtrrdi
StepHypRef Expression
1 sseqtrrdi.1 . 2 (𝜑𝐴𝐵)
2 sseqtrrdi.2 . . 3 𝐶 = 𝐵
32eqcomi 2197 . 2 𝐵 = 𝐶
41, 3sseqtrdi 3227 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1364  wss 3153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166
This theorem is referenced by:  iunpw  4511  iotanul  5230  iotass  5232  tfrlem9  6372  tfrlemibfn  6381  tfrlemiubacc  6383  tfrlemi14d  6386  tfr1onlemssrecs  6392  tfr1onlemres  6402  tfrcllemres  6415  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  uznnssnn  9642  shftfvalg  10962  shftfval  10965  clim2prod  11682  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrex  13594  eltopss  14177  difopn  14276  tgrest  14337  txuni2  14424  tgioo  14714
  Copyright terms: Public domain W3C validator