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

Theorem 3imtr4g 203
Description: More general version of 3imtr4i 199. 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 150 . 2  |-  ( ph  ->  ( th  ->  ch ) )
4 3imtr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6ibr 160 1  |-  ( ph  ->  ( th  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3anim123d  1251  3orim123d  1252  hbbid  1508  spsbim  1765  moim  2006  moimv  2008  2euswapdc  2033  ralim  2423  ralimdaa  2429  ralimdv2  2432  rexim  2456  reximdv2  2461  rmoim  2792  ssel  2994  sstr2  3007  sscon  3107  ssdif  3108  unss1  3142  ssrin  3198  prel12  3571  uniss  3630  ssuni  3631  intss  3665  intssunim  3666  iunss1  3697  iinss1  3698  ss2iun  3701  disjss2  3777  disjss1  3780  ssbrd  3834  sspwb  3979  poss  4061  pofun  4075  soss  4077  sess1  4100  sess2  4101  ordwe  4326  wessep  4328  peano2  4344  finds  4349  finds2  4350  relss  4453  ssrel  4454  ssrel2  4456  ssrelrel  4466  xpsspw  4478  relop  4514  cnvss  4536  dmss  4562  dmcosseq  4631  funss  4950  imadif  5010  imain  5012  fss  5085  fun  5094  brprcneu  5202  isores3  5486  isopolem  5492  isosolem  5494  tposfn2  5915  tposfo2  5916  tposf1o2  5919  smores  5941  tfr1onlemaccex  5997  tfrcllemaccex  6010  iinerm  6244  xpdom2  6375  recexprlemlol  6878  recexprlemupu  6880  axpre-ltwlin  7111  axpre-apti  7113  nnindnn  7121  nnind  8122  uzind  8539  cau3lem  10138
  Copyright terms: Public domain W3C validator