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

Theorem sylan9eqr 2091
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.)
Hypotheses
Ref Expression
sylan9eqr.1 (φA = B)
sylan9eqr.2 (ψB = 𝐶)
Assertion
Ref Expression
sylan9eqr ((ψ φ) → A = 𝐶)

Proof of Theorem sylan9eqr
StepHypRef Expression
1 sylan9eqr.1 . . 3 (φA = B)
2 sylan9eqr.2 . . 3 (ψB = 𝐶)
31, 2sylan9eq 2089 . 2 ((φ ψ) → A = 𝐶)
43ancoms 255 1 ((ψ φ) → A = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1242
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  sbcied2  2794  csbied2  2887  fun2ssres  4886  fcoi1  5013  fcoi2  5014  funssfv  5142  caovimo  5636  mpt2mptsx  5765  dmmpt2ssx  5767  fmpt2x  5768  2ndconst  5785  mpt2xopoveq  5796  tfrlemisucaccv  5880  rdgivallem  5908  nnmass  6005  nnm00  6038  ltexnqq  6391  ltrnqg  6403  nqnq0a  6437  nqnq0m  6438  nq0m0r  6439  nq0a0  6440  addnqprllem  6510  addnqprulem  6511  nnnn0addcl  7988  zindd  8132  qaddcl  8346  qmulcl  8348  qreccl  8351  frec2uzrdg  8876  expp1  8916  expnegap0  8917  expcllem  8920  mulexp  8948  expmul  8954  reim0b  9090  cjexp  9121
  Copyright terms: Public domain W3C validator