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

Theorem sylan9eqr 2110
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
Hypotheses
Ref Expression
sylan9eqr.1  |-  ( ph  ->  A  =  B )
sylan9eqr.2  |-  ( ps 
->  B  =  C
)
Assertion
Ref Expression
sylan9eqr  |-  ( ( ps  /\  ph )  ->  A  =  C )

Proof of Theorem sylan9eqr
StepHypRef Expression
1 sylan9eqr.1 . . 3  |-  ( ph  ->  A  =  B )
2 sylan9eqr.2 . . 3  |-  ( ps 
->  B  =  C
)
31, 2sylan9eq 2108 . 2  |-  ( (
ph  /\  ps )  ->  A  =  C )
43ancoms 259 1  |-  ( ( ps  /\  ph )  ->  A  =  C )
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  2823  csbied2  2921  fun2ssres  4971  fcoi1  5098  fcoi2  5099  funssfv  5227  caovimo  5722  mpt2mptsx  5851  dmmpt2ssx  5853  fmpt2x  5854  2ndconst  5871  mpt2xopoveq  5886  tfrlemisucaccv  5970  rdgivallem  5999  nnmass  6097  nnm00  6133  ltexnqq  6564  ltrnqg  6576  nqnq0a  6610  nqnq0m  6611  nq0m0r  6612  nq0a0  6613  addnqprllem  6683  addnqprulem  6684  rereceu  7021  addid0  7443  nnnn0addcl  8269  zindd  8415  qaddcl  8667  qmulcl  8669  qreccl  8674  modfzo0difsn  9345  frec2uzrdg  9359  expp1  9427  expnegap0  9428  expcllem  9431  mulexp  9459  expmul  9465  sqoddm1div8  9569  bcpasc  9634  shftfn  9653  reim0b  9690  cjexp  9721  dvdsnegb  10125  m1expe  10211  m1expo  10212  m1exp1  10213  flodddiv4  10246
  Copyright terms: Public domain W3C validator