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

Theorem 3imtr4i 199
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 119 . 2  |-  ( ch 
->  ps )
4 3imtr4.3 . 2  |-  ( th  <->  ps )
53, 4sylibr 132 1  |-  ( ch 
->  th )
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:  dcn  782  dcan  878  xordc1  1327  hbxfrbi  1404  nfalt  1513  19.29r  1555  19.31r  1614  sbimi  1691  spsbbi  1769  sbi2v  1817  euan  2001  2exeu  2037  ralimi2  2431  reximi2  2465  r19.28av  2501  r19.29r  2503  elex  2624  rmoan  2804  rmoimi2  2807  sseq2  3037  rabss2  3093  unssdif  3223  inssdif  3224  unssin  3227  inssun  3228  rabn0r  3298  undif4  3333  ssdif0im  3335  inssdif0im  3338  ssundifim  3353  ralf0  3372  prmg  3544  difprsnss  3558  snsspw  3591  pwprss  3632  pwtpss  3633  uniin  3656  intss  3692  iuniin  3723  iuneq1  3726  iuneq2  3729  iundif2ss  3778  iinuniss  3793  iunpwss  3799  intexrabim  3964  exmidundif  4009  exss  4028  pwunss  4084  soeq2  4117  ordunisuc2r  4304  peano5  4386  reliin  4527  coeq1  4561  coeq2  4562  cnveq  4578  dmeq  4604  dmin  4612  dmcoss  4670  rncoeq  4674  resiexg  4724  dminss  4812  imainss  4813  dfco2a  4897  euiotaex  4962  fununi  5047  fof  5196  f1ocnv  5229  rexrnmpt  5405  isocnv  5551  isotr  5556  oprabid  5638  dmtpos  5975  tposfn  5992  smores  6011  eqer  6276  enssdom  6431  fiprc  6484  ltexprlemlol  7105  ltexprlemupu  7107  recexgt0  7998  peano2uz2  8786  eluzp1p1  8976  peano2uz  9003  zq  9043  ubmelfzo  9539  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  expclzaplem  9877  hashfiv01gt1  10086  qredeu  10954  bj-indint  11264
  Copyright terms: Public domain W3C validator