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

Theorem 3imtr4g 204
Description: More general version of 3imtr4i 200. 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  |-  ( ph  ->  ( ps  ->  ch ) )
3imtr4g.2  |-  ( th  <->  ps )
3imtr4g.3  |-  ( ta  <->  ch )
Assertion
Ref Expression
3imtr4g  |-  ( ph  ->  ( th  ->  ta ) )

Proof of Theorem 3imtr4g
StepHypRef Expression
1 3imtr4g.2 . . 3  |-  ( th  <->  ps )
2 3imtr4g.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5bi 151 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 161 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3anim123d  1297  3orim123d  1298  hbbid  1554  spsbim  1815  moim  2063  moimv  2065  2euswapdc  2090  nelcon3d  2414  ralim  2491  ralimdaa  2498  ralimdv2  2502  rexim  2526  reximdv2  2531  rmoim  2885  ssel  3091  sstr2  3104  ssrexf  3159  ssrmof  3160  sscon  3210  ssdif  3211  unss1  3245  ssrin  3301  prel12  3701  uniss  3760  ssuni  3761  intss  3795  intssunim  3796  iunss1  3827  iinss1  3828  ss2iun  3831  disjss2  3912  disjss1  3915  ssbrd  3974  sspwb  4141  poss  4223  pofun  4237  soss  4239  sess1  4262  sess2  4263  ordwe  4493  wessep  4495  peano2  4512  finds  4517  finds2  4518  relss  4629  ssrel  4630  ssrel2  4632  ssrelrel  4642  xpsspw  4654  relop  4692  cnvss  4715  dmss  4741  dmcosseq  4813  funss  5145  imadif  5206  imain  5208  fss  5287  fun  5298  brprcneu  5417  isores3  5719  isopolem  5726  isosolem  5728  tposfn2  6166  tposfo2  6167  tposf1o2  6170  smores  6192  tfr1onlemaccex  6248  tfrcllemaccex  6261  iinerm  6504  xpdom2  6728  ssenen  6748  exmidpw  6805  recexprlemlol  7453  recexprlemupu  7455  axpre-ltwlin  7710  axpre-apti  7712  nnindnn  7720  nnind  8755  uzind  9181  hashfacen  10603  cau3lem  10910  tgcl  12259  epttop  12285  txcnp  12466
  Copyright terms: Public domain W3C validator