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

Theorem sylan9eqr 2136
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 2134 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 264 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  sbcied2  2852  csbied2  2950  fun2ssres  4967  fcoi1  5095  fcoi2  5096  funssfv  5225  caovimo  5719  mpt2mptsx  5848  dmmpt2ssx  5850  fmpt2x  5851  2ndconst  5868  mpt2xopoveq  5883  tfrlemisucaccv  5968  tfr1onlemsucaccv  5984  tfrcllemsucaccv  5997  rdgivallem  6024  nnmass  6124  nnm00  6161  ltexnqq  6649  ltrnqg  6661  nqnq0a  6695  nqnq0m  6696  nq0m0r  6697  nq0a0  6698  addnqprllem  6768  addnqprulem  6769  rereceu  7106  addid0  7533  nnnn0addcl  8374  zindd  8535  qaddcl  8790  qmulcl  8792  qreccl  8797  modfzo0difsn  9466  frec2uzrdg  9480  expp1  9569  expnegap0  9570  expcllem  9573  mulexp  9601  expmul  9607  sqoddm1div8  9711  bcpasc  9779  shftfn  9839  reim0b  9876  cjexp  9907  dvdsnegb  10346  m1expe  10432  m1expo  10433  m1exp1  10434  flodddiv4  10467  gcdabs  10512  bezoutr1  10555  dvdslcm  10584  lcmeq0  10586  lcmcl  10587  lcmabs  10591  lcmgcdlem  10592  lcmdvds  10594  mulgcddvds  10609  qredeu  10612  divgcdcoprmex  10617
  Copyright terms: Public domain W3C validator