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  1253  3orim123d  1254  hbbid  1510  spsbim  1768  moim  2009  moimv  2011  2euswapdc  2036  ralim  2430  ralimdaa  2436  ralimdv2  2439  rexim  2463  reximdv2  2468  rmoim  2805  ssel  3008  sstr2  3021  sscon  3123  ssdif  3124  unss1  3158  ssrin  3214  prel12  3597  uniss  3656  ssuni  3657  intss  3691  intssunim  3692  iunss1  3723  iinss1  3724  ss2iun  3727  disjss2  3803  disjss1  3806  ssbrd  3860  sspwb  4015  poss  4097  pofun  4111  soss  4113  sess1  4136  sess2  4137  ordwe  4362  wessep  4364  peano2  4381  finds  4386  finds2  4387  relss  4491  ssrel  4492  ssrel2  4494  ssrelrel  4504  xpsspw  4516  relop  4552  cnvss  4575  dmss  4601  dmcosseq  4670  funss  4995  imadif  5055  imain  5057  fss  5131  fun  5140  brprcneu  5254  isores3  5548  isopolem  5555  isosolem  5557  tposfn2  5978  tposfo2  5979  tposf1o2  5982  smores  6004  tfr1onlemaccex  6060  tfrcllemaccex  6073  iinerm  6309  xpdom2  6492  ssenen  6512  exmidpw  6569  recexprlemlol  7121  recexprlemupu  7123  axpre-ltwlin  7354  axpre-apti  7356  nnindnn  7364  nnind  8365  uzind  8782  hashfacen  10129  cau3lem  10434
  Copyright terms: Public domain W3C validator