New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  3imtr4g GIF version

Theorem 3imtr4g 261
 Description: More general version of 3imtr4i 257. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypotheses
Ref Expression
3imtr4g.1 (φ → (ψχ))
3imtr4g.2 (θψ)
3imtr4g.3 (τχ)
Assertion
Ref Expression
3imtr4g (φ → (θτ))

Proof of Theorem 3imtr4g
StepHypRef Expression
1 3imtr4g.2 . . 3 (θψ)
2 3imtr4g.1 . . 3 (φ → (ψχ))
31, 2syl5bi 208 . 2 (φ → (θχ))
4 3imtr4g.3 . 2 (τχ)
53, 4syl6ibr 218 1 (φ → (θτ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  3anim123d  1259  3orim123d  1260  moim  2250  morimv  2252  2euswap  2280  ralim  2685  ralimdaa  2691  ralimdv2  2694  rexim  2718  reximdv2  2723  moeq3  3013  rmoim  3035  2reuswap  3038  ssel  3267  sstr2  3279  sscon  3400  ssdif  3401  unss1  3432  ssrin  3480  difin0ss  3616  r19.2z  3639  uniss  3912  ssuni  3913  intss  3947  intssuni  3948  iunss1  3980  iinss1  3981  ss2iun  3984  sspwb  4118  findsd  4410  ncfinlower  4483  evenoddnnnul  4514  spfinsfincl  4539  vfinspss  4551  vfinspclt  4552  vinf  4555  ssbrd  4680  ssrel  4844  cnvss  4885  dmss  4906  dmcosseq  4973  funss  5126  fss  5230  fun  5236  eqfnfv  5392  clos1conn  5879  clos1is  5881  enadjlem1  6059  enprmaplem6  6081  leltctr  6212  nnltp1c  6262  nncdiv3  6277  spacind  6287  nchoicelem17  6305
 Copyright terms: Public domain W3C validator