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

Theorem sylan9eqr 2110
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 2108 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 259 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  sbcied2  2822  csbied2  2920  fun2ssres  4970  fcoi1  5097  fcoi2  5098  funssfv  5226  caovimo  5721  mpt2mptsx  5850  dmmpt2ssx  5852  fmpt2x  5853  2ndconst  5870  mpt2xopoveq  5885  tfrlemisucaccv  5969  rdgivallem  5998  nnmass  6096  nnm00  6132  ltexnqq  6563  ltrnqg  6575  nqnq0a  6609  nqnq0m  6610  nq0m0r  6611  nq0a0  6612  addnqprllem  6682  addnqprulem  6683  rereceu  7020  addid0  7442  nnnn0addcl  8268  zindd  8414  qaddcl  8666  qmulcl  8668  qreccl  8673  modfzo0difsn  9339  frec2uzrdg  9353  expp1  9421  expnegap0  9422  expcllem  9425  mulexp  9453  expmul  9459  sqoddm1div8  9562  bcpasc  9627  shftfn  9646  reim0b  9683  cjexp  9714  dvdsnegb  10117  m1expe  10203  m1expo  10204  m1exp1  10205
  Copyright terms: Public domain W3C validator