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

Theorem sylan9eqr 2094
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
Hypotheses
Ref Expression
sylan9eqr.1 (𝜑𝐴 = 𝐵)
sylan9eqr.2 (𝜓𝐵 = 𝐶)
Assertion
Ref Expression
sylan9eqr ((𝜓𝜑) → 𝐴 = 𝐶)

Proof of Theorem sylan9eqr
StepHypRef Expression
1 sylan9eqr.1 . . 3 (𝜑𝐴 = 𝐵)
2 sylan9eqr.2 . . 3 (𝜓𝐵 = 𝐶)
31, 2sylan9eq 2092 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 255 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97   = wceq 1243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  sbcied2  2800  csbied2  2893  fun2ssres  4943  fcoi1  5070  fcoi2  5071  funssfv  5199  caovimo  5694  mpt2mptsx  5823  dmmpt2ssx  5825  fmpt2x  5826  2ndconst  5843  mpt2xopoveq  5855  tfrlemisucaccv  5939  rdgivallem  5968  nnmass  6066  nnm00  6102  ltexnqq  6506  ltrnqg  6518  nqnq0a  6552  nqnq0m  6553  nq0m0r  6554  nq0a0  6555  addnqprllem  6625  addnqprulem  6626  rereceu  6963  nnnn0addcl  8212  zindd  8356  qaddcl  8570  qmulcl  8572  qreccl  8576  frec2uzrdg  9195  expp1  9262  expnegap0  9263  expcllem  9266  mulexp  9294  expmul  9300  shftfn  9425  reim0b  9462  cjexp  9493
  Copyright terms: Public domain W3C validator