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  737  dcimptest  744  dcan  830  xordc1  1267  hbxfrbi  1341  nfalt  1452  19.29r  1494  19.31r  1553  sbimi  1629  spsbbi  1707  sbi2v  1754  euan  1938  2exeu  1974  ralimi2  2359  reximi2  2393  r19.28av  2427  r19.29r  2429  elex  2543  rmoan  2716  rmoimi2  2719  sseq2  2944  rabss2  3000  unssdif  3149  inssdif  3150  unssin  3153  inssun  3154  rabn0r  3221  undif4  3261  ssdif0im  3263  inssdif0im  3268  ssundifim  3283  ralf0  3303  prmg  3463  difprsnss  3476  snsspw  3509  pwprss  3550  pwtpss  3551  uniin  3574  intss  3610  iuniin  3641  iuneq1  3644  iuneq2  3647  iundif2ss  3696  iinuniss  3711  iunpwss  3717  intexrabim  3881  exss  3937  pwunss  3994  soeq2  4027  ordunisuc2r  4189  peano5  4248  reliin  4386  coeq1  4420  coeq2  4421  cnveq  4436  dmeq  4462  dmin  4470  dmcoss  4528  rncoeq  4532  resiexg  4580  dminss  4665  imainss  4666  dfco2a  4748  euiotaex  4810  fununi  4893  fof  5031  f1ocnv  5064  rexrnmpt  5235  isocnv  5376  isotr  5381  oprabid  5461  dmtpos  5793  tposfn  5810  smores  5829  eqer  6049  ltexprlemlol  6439  ltexprlemupu  6441  bj-indint  7154  peano5set  7162
  Copyright terms: Public domain W3C validator