ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3imtr4i GIF 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 (𝜑𝜓)
3imtr4.2 (𝜒𝜑)
3imtr4.3 (𝜃𝜓)
Assertion
Ref Expression
3imtr4i (𝜒𝜃)

Proof of Theorem 3imtr4i
StepHypRef Expression
1 3imtr4.2 . . 3 (𝜒𝜑)
2 3imtr4.1 . . 3 (𝜑𝜓)
31, 2sylbi 120 . 2 (𝜒𝜓)
4 3imtr4.3 . 2 (𝜃𝜓)
53, 4sylibr 133 1 (𝜒𝜃)
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  812  stdcn  817  dcan  903  xordc1  1356  hbxfrbi  1433  nfalt  1542  19.29r  1585  19.31r  1644  sbimi  1722  spsbbi  1800  sbi2v  1848  euan  2033  2exeu  2069  ralimi2  2469  reximi2  2505  r19.28av  2545  r19.29r  2547  elex  2671  rmoan  2857  rmoimi2  2860  sseq2  3091  rabss2  3150  unssdif  3281  inssdif  3282  unssin  3285  inssun  3286  rabn0r  3359  undif4  3395  ssdif0im  3397  inssdif0im  3400  ssundifim  3416  ralf0  3436  prmg  3614  difprsnss  3628  snsspw  3661  pwprss  3702  pwtpss  3703  uniin  3726  intss  3762  iuniin  3793  iuneq1  3796  iuneq2  3799  iundif2ss  3848  iinuniss  3865  iunpwss  3874  intexrabim  4048  exmidundif  4099  exmidundifim  4100  exss  4119  pwunss  4175  soeq2  4208  ordunisuc2r  4400  peano5  4482  reliin  4631  coeq1  4666  coeq2  4667  cnveq  4683  dmeq  4709  dmin  4717  dmcoss  4778  rncoeq  4782  resiexg  4834  dminss  4923  imainss  4924  dfco2a  5009  euiotaex  5074  fununi  5161  fof  5315  f1ocnv  5348  rexrnmpt  5531  isocnv  5680  isotr  5685  oprabid  5771  dmtpos  6121  tposfn  6138  smores  6157  eqer  6429  ixpeq2  6574  enssdom  6624  fiprc  6677  fiintim  6785  ltexprlemlol  7378  ltexprlemupu  7380  recexgt0  8310  peano2uz2  9126  eluzp1p1  9319  peano2uz  9346  zq  9386  ubmelfzo  9945  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  expclzaplem  10285  hashfiv01gt1  10496  fsum2dlemstep  11171  sin02gt0  11397  qredeu  11705  bj-stim  12881  bj-stan  12882  bj-stal  12884  bj-nfalt  12898  bj-indint  13056
  Copyright terms: Public domain W3C validator