ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan9eqr Structured version   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  6436  nqnq0m  6437  nq0m0r  6438  nq0a0  6439  addnqprllem  6509  addnqprulem  6510  nnnn0addcl  7968  zindd  8112  qaddcl  8326  qmulcl  8328  qreccl  8331  frec2uzrdg  8856  expp1  8896  expnegap0  8897  expcllem  8900  mulexp  8928  expmul  8934  reim0b  9070  cjexp  9101
  Copyright terms: Public domain W3C validator