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

Theorem sylan9eqr 2194
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 2192 . 2 ((𝜑𝜓) → 𝐴 = 𝐶)
43ancoms 266 1 ((𝜓𝜑) → 𝐴 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  sbcied2  2946  csbied2  3047  fun2ssres  5166  fcoi1  5303  fcoi2  5304  funssfv  5447  caovimo  5964  mpomptsx  6095  dmmpossx  6097  fmpox  6098  2ndconst  6119  mpoxopoveq  6137  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  rdgivallem  6278  nnmass  6383  nnm00  6425  ssenen  6745  fi0  6863  exmidfodomrlemim  7062  ltexnqq  7228  ltrnqg  7240  nqnq0a  7274  nqnq0m  7275  nq0m0r  7276  nq0a0  7277  addnqprllem  7347  addnqprulem  7348  map2psrprg  7625  rereceu  7709  addid0  8147  nnnn0addcl  9019  zindd  9181  qaddcl  9439  qmulcl  9441  qreccl  9446  xaddpnf1  9641  xaddmnf1  9643  xaddnemnf  9652  xaddnepnf  9653  xaddcom  9656  xnegdi  9663  xaddass  9664  xpncan  9666  xleadd1a  9668  xltadd1  9671  xlt2add  9675  modfzo0difsn  10180  frec2uzrdg  10194  expp1  10312  expnegap0  10313  expcllem  10316  mulexp  10344  expmul  10350  sqoddm1div8  10456  bcpasc  10524  hashfzo  10580  shftfn  10608  reim0b  10646  cjexp  10677  sumsnf  11190  binomlem  11264  ef0lem  11378  dvdsnegb  11521  m1expe  11607  m1expo  11608  m1exp1  11609  flodddiv4  11642  gcdabs  11687  bezoutr1  11732  dvdslcm  11761  lcmeq0  11763  lcmcl  11764  lcmabs  11768  lcmgcdlem  11769  lcmdvds  11771  mulgcddvds  11786  qredeu  11789  divgcdcoprmex  11794  isxmet2d  12531  blfvalps  12568  blssioo  12728  efper  12910
  Copyright terms: Public domain W3C validator