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

Theorem 3imtr4i 201
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 121 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 134 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  dcn  843  stdcn  848  xordc1  1404  hbxfrbi  1483  nfalt  1589  19.29r  1632  19.31r  1692  sbimi  1775  spsbbi  1855  sbi2v  1904  euan  2098  2exeu  2134  ralimi2  2554  reximi2  2590  r19.28av  2630  r19.29r  2632  elex  2771  rmoan  2961  rmoimi2  2964  sseq2  3204  rabss2  3263  unssdif  3395  inssdif  3396  unssin  3399  inssun  3400  rabn0r  3474  undif4  3510  ssdif0im  3512  inssdif0im  3515  ssundifim  3531  ralf0  3550  prmg  3740  difprsnss  3757  snsspw  3791  pwprss  3832  pwtpss  3833  uniin  3856  intss  3892  iuniin  3923  iuneq1  3926  iuneq2  3929  iundif2ss  3979  iinuniss  3996  iunpwss  4005  intexrabim  4183  exmidundif  4236  exmidundifim  4237  exss  4257  pwunss  4315  soeq2  4348  ordunisuc2r  4547  peano5  4631  reliin  4782  coeq1  4820  coeq2  4821  cnveq  4837  dmeq  4863  dmin  4871  dmcoss  4932  rncoeq  4936  resiexg  4988  dminss  5081  imainss  5082  dfco2a  5167  euiotaex  5232  eliotaeu  5244  fununi  5323  fof  5477  f1ocnv  5514  rexrnmpt  5702  isocnv  5855  isotr  5860  oprabid  5951  dmtpos  6311  tposfn  6328  smores  6347  eqer  6621  ixpeq2  6768  enssdom  6818  fiprc  6871  fiintim  6987  ltexprlemlol  7664  ltexprlemupu  7666  recexgt0  8601  peano2uz2  9427  eluzp1p1  9621  peano2uz  9651  zq  9694  ubmelfzo  10270  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  expclzaplem  10637  hashfiv01gt1  10856  wrdeq  10939  fsum2dlemstep  11580  fprod2dlemstep  11768  sin02gt0  11910  qredeu  12238  prmdc  12271  subrngrng  13701  lgslem3  15159  bj-stim  15308  bj-stan  15309  bj-stal  15311  bj-nfalt  15326  bj-indint  15493  tridceq  15616
  Copyright terms: Public domain W3C validator