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

Theorem 3imtr4i 200
Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3imtr4.1  |-  ( ph  ->  ps )
3imtr4.2  |-  ( ch  <->  ph )
3imtr4.3  |-  ( th  <->  ps )
Assertion
Ref Expression
3imtr4i  |-  ( ch 
->  th )

Proof of Theorem 3imtr4i
StepHypRef Expression
1 3imtr4.2 . . 3  |-  ( ch  <->  ph )
2 3imtr4.1 . . 3  |-  ( ph  ->  ps )
31, 2sylbi 120 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 133 1  |-  ( ch 
->  th )
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:  dcn  828  stdcn  833  dcan  919  xordc1  1372  hbxfrbi  1449  nfalt  1558  19.29r  1601  19.31r  1660  sbimi  1738  spsbbi  1817  sbi2v  1865  euan  2056  2exeu  2092  ralimi2  2495  reximi2  2531  r19.28av  2571  r19.29r  2573  elex  2700  rmoan  2887  rmoimi2  2890  sseq2  3125  rabss2  3184  unssdif  3315  inssdif  3316  unssin  3319  inssun  3320  rabn0r  3393  undif4  3429  ssdif0im  3431  inssdif0im  3434  ssundifim  3450  ralf0  3470  prmg  3651  difprsnss  3665  snsspw  3698  pwprss  3739  pwtpss  3740  uniin  3763  intss  3799  iuniin  3830  iuneq1  3833  iuneq2  3836  iundif2ss  3885  iinuniss  3902  iunpwss  3911  intexrabim  4085  exmidundif  4136  exmidundifim  4137  exss  4156  pwunss  4212  soeq2  4245  ordunisuc2r  4437  peano5  4519  reliin  4668  coeq1  4703  coeq2  4704  cnveq  4720  dmeq  4746  dmin  4754  dmcoss  4815  rncoeq  4819  resiexg  4871  dminss  4960  imainss  4961  dfco2a  5046  euiotaex  5111  fununi  5198  fof  5352  f1ocnv  5387  rexrnmpt  5570  isocnv  5719  isotr  5724  oprabid  5810  dmtpos  6160  tposfn  6177  smores  6196  eqer  6468  ixpeq2  6613  enssdom  6663  fiprc  6716  fiintim  6824  ltexprlemlol  7433  ltexprlemupu  7435  recexgt0  8365  peano2uz2  9181  eluzp1p1  9374  peano2uz  9404  zq  9444  ubmelfzo  10007  frecuzrdgtcl  10215  frecuzrdgfunlem  10222  expclzaplem  10347  hashfiv01gt1  10559  fsum2dlemstep  11234  sin02gt0  11504  qredeu  11812  bj-stim  13123  bj-stan  13124  bj-stal  13126  bj-nfalt  13140  bj-indint  13298
  Copyright terms: Public domain W3C validator