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

Theorem syl5ibr 154
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.)
Hypotheses
Ref Expression
syl5ibr.1  |-  ( ph  ->  th )
syl5ibr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibr  |-  ( ch 
->  ( ph  ->  ps ) )

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2  |-  ( ph  ->  th )
2 syl5ibr.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32bicomd 139 . 2  |-  ( ch 
->  ( th  <->  ps )
)
41, 3syl5ib 152 1  |-  ( ch 
->  ( ph  ->  ps ) )
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  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  syl5ibrcom  155  biimprd  156  nbn2  648  limelon  4217  eldifpw  4289  ssonuni  4295  onsucuni2  4370  peano2  4400  limom  4418  elrnmpt1  4674  cnveqb  4873  cnveq0  4874  relcoi1  4949  ndmfvg  5319  ffvresb  5445  caovord3d  5797  poxp  5979  nnm0r  6222  nnacl  6223  nnacom  6227  nnaass  6228  nndi  6229  nnmass  6230  nnmsucr  6231  nnmcom  6232  brecop  6362  ecopovtrn  6369  ecopovtrng  6372  elpm2r  6403  map0g  6425  fundmen  6503  mapxpen  6544  phpm  6561  f1vrnfibi  6633  mulcmpblnq  6906  ordpipqqs  6912  mulcmpblnq0  6982  genpprecll  7052  genppreclu  7053  addcmpblnr  7264  ax1rid  7391  axpre-mulgt0  7401  cnegexlem1  7636  msqge0  8069  mulge0  8072  ltleap  8083  nnmulcl  8415  nnsub  8432  elnn0z  8733  ztri3or0  8762  nneoor  8818  uz11  9010  xltnegi  9266  frec2uzuzd  9774  iseqsst  9850  iseqfveq2  9854  seq3fveq2  9856  iseqshft2  9862  seq3split  9872  iseqsplit  9873  iseqcaopr3  9875  iseqid2  9905  iseqhomo  9906  seq3homo  9908  m1expcl2  9941  expadd  9961  expmul  9964  faclbnd  10113  hashfzp1  10196  hashfacen  10205  iseqcoll  10211  caucvgrelemcau  10377  recan  10506  rexanre  10617  fsumiun  10831  dvdstr  10913  alzdvds  10935  zob  10971  gcdmultiplez  11090  dvdssq  11100  cncongr2  11166  bj-om  11476  bj-inf2vnlem2  11510  bj-inf2vn  11513  bj-inf2vn2  11514
  Copyright terms: Public domain W3C validator