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

Theorem syl6bi 161
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
Hypotheses
Ref Expression
syl6bi.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6bi.2  |-  ( ch 
->  th )
Assertion
Ref Expression
syl6bi  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6bi
StepHypRef Expression
1 syl6bi.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 142 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bi.2 . 2  |-  ( ch 
->  th )
42, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  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
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  19.33bdc  1562  ax11i  1643  equveli  1683  eupickbi  2024  rgen2a  2418  reu6  2782  sseq0  3292  disjel  3305  preq12b  3570  prel12  3571  prneimg  3574  elinti  3653  opthreg  4307  elreldm  4588  issref  4737  relcnvtr  4870  relresfld  4877  funopg  4964  funimass2  5008  fvimacnv  5314  elunirn  5437  oprabid  5568  op1steq  5836  f1o2ndf1  5880  reldmtpos  5902  rntpos  5906  nntri3or  6137  nnaordex  6166  nnawordex  6167  findcard2  6423  findcard2s  6424  lt2addnq  6656  lt2mulnq  6657  genpelvl  6764  genpelvu  6765  distrlem5prl  6838  distrlem5pru  6839  caucvgprlemnkj  6918  rereceu  7117  ltxrlt  7245  0mnnnnn0  8387  elnnnn0b  8399  btwnz  8547  uz11  8722  nn01to3  8783  zq  8792  xrltso  8947  xltnegi  8978  iccleub  9030  fzdcel  9135  uznfz  9196  2ffzeq  9228  elfzonlteqm1  9296  flqeqceilz  9400  modqadd1  9443  modqmul1  9459  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  fzfig  9512  m1expeven  9620  caucvgrelemcau  10004  rexico  10245  0dvds  10360  alzdvds  10399  opoe  10439  omoe  10440  opeo  10441  omeo  10442  m1exp1  10445  nn0enne  10446  nn0o1gt2  10449  gcdneg  10517  dfgcd2  10547  algcvgblem  10575  ialgcvga  10577  eucalglt  10583  coprmdvds  10618  divgcdcoprmex  10628  cncongr1  10629  prm2orodd  10652  bj-elssuniab  10752  bj-nn0sucALT  10931
  Copyright terms: Public domain W3C validator