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

Theorem 3imtr4i 190
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 (φψ)
3imtr4.2 (χφ)
3imtr4.3 (θψ)
Assertion
Ref Expression
3imtr4i (χθ)

Proof of Theorem 3imtr4i
StepHypRef Expression
1 3imtr4.2 . . 3 (χφ)
2 3imtr4.1 . . 3 (φψ)
31, 2sylbi 114 . 2 (χψ)
4 3imtr4.3 . 2 (θψ)
53, 4sylibr 137 1 (χθ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  dcn  745  dcan  841  xordc1  1281  hbxfrbi  1358  nfalt  1467  19.29r  1509  19.31r  1568  sbimi  1644  spsbbi  1722  sbi2v  1769  euan  1953  2exeu  1989  ralimi2  2375  reximi2  2409  r19.28av  2443  r19.29r  2445  elex  2560  rmoan  2733  rmoimi2  2736  sseq2  2961  rabss2  3017  unssdif  3166  inssdif  3167  unssin  3170  inssun  3171  rabn0r  3238  undif4  3278  ssdif0im  3280  inssdif0im  3285  ssundifim  3300  ralf0  3318  prmg  3480  difprsnss  3493  snsspw  3526  pwprss  3567  pwtpss  3568  uniin  3591  intss  3627  iuniin  3658  iuneq1  3661  iuneq2  3664  iundif2ss  3713  iinuniss  3728  iunpwss  3734  intexrabim  3898  exss  3954  pwunss  4011  soeq2  4044  ordunisuc2r  4205  peano5  4264  reliin  4402  coeq1  4436  coeq2  4437  cnveq  4452  dmeq  4478  dmin  4486  dmcoss  4544  rncoeq  4548  resiexg  4596  dminss  4681  imainss  4682  dfco2a  4764  euiotaex  4826  fununi  4910  fof  5049  f1ocnv  5082  rexrnmpt  5253  isocnv  5394  isotr  5399  oprabid  5480  dmtpos  5812  tposfn  5829  smores  5848  eqer  6074  enssdom  6178  fiprc  6228  ltexprlemlol  6575  ltexprlemupu  6577  recexgt0  7344  peano2uz2  8101  eluzp1p1  8254  peano2uz  8282  zq  8317  elfzmlbmOLD  8739  ubmelfzo  8806  frecuzrdgfn  8859  expclzaplem  8913  bj-indint  9366  peano5set  9374
  Copyright terms: Public domain W3C validator