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

Theorem syl5ibcom 155
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
imbitrid.1  |-  ( ph  ->  ps )
imbitrid.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibcom  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem syl5ibcom
StepHypRef Expression
1 imbitrid.1 . . 3  |-  ( ph  ->  ps )
2 imbitrid.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
31, 2imbitrid 154 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 30 1  |-  ( ph  ->  ( 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
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biimpcd  159  mob2  2917  rmob  3055  preqr1g  3764  issod  4315  sotritrieq  4321  nsuceq0g  4414  suctr  4417  nordeq  4539  suc11g  4552  iss  4948  poirr2  5016  xp11m  5062  tz6.12c  5540  fnbrfvb  5551  fvelimab  5567  foeqcnvco  5784  f1eqcocnv  5785  acexmidlemcase  5863  nna0r  6472  nnawordex  6523  ectocld  6594  ecoptocl  6615  mapsn  6683  eqeng  6759  fopwdom  6829  ordiso  7028  ltexnqq  7385  nsmallnqq  7389  nqprloc  7522  aptiprleml  7616  map2psrprg  7782  0re  7935  lttri3  8014  0cnALT  8124  reapti  8513  recnz  9322  zneo  9330  uzn0  9519  flqidz  10259  ceilqidz  10289  modqid2  10324  modqmuladdnn0  10341  frec2uzrand  10378  frecuzrdgtcl  10385  seq3id  10481  seq3z  10484  facdiv  10689  facwordi  10691  maxleb  11196  fsumf1o  11369  dvdsnegb  11786  odd2np1lem  11847  odd2np1  11848  ltoddhalfle  11868  halfleoddlt  11869  opoe  11870  omoe  11871  opeo  11872  omeo  11873  gcddiv  11990  gcdzeq  11993  dvdssqim  11995  lcmgcdeq  12053  coprmdvds2  12063  rpmul  12068  divgcdcoprmex  12072  cncongr2  12074  dvdsprm  12107  coprm  12114  prmdvdsexp  12118  prmdiv  12205  pythagtriplem19  12252  pc2dvds  12299  pcadd  12309  prmpwdvds  12323  exmidunben  12397  intopsn  12665  ismgmid  12675  isgrpid2  12790  isgrpinv  12803  dfgrp3mlem  12844  dvdsrcl2  13080  dvdsrtr  13082  dvdsrmul1  13083  baspartn  13181  bastop  13208  isopn3  13258  lgsdir  14069  lgsne0  14072  bj-peano4  14329  sbthomlem  14396
  Copyright terms: Public domain W3C validator