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

Theorem syl5bi 150
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bi.1  |-  ( ph  <->  ps )
syl5bi.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5bi  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3  |-  ( ph  <->  ps )
21biimpi 118 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  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:  3imtr4g  203  ancomsd  265  pm2.13dc  817  3jao  1237  19.33b2  1565  sbequ2  1699  sbi1v  1819  mor  1990  2euex  2035  eqneqall  2265  necon3ad  2297  necon1aidc  2306  necon4addc  2325  spcimgft  2695  spcimegft  2697  rspc  2716  rspcimdv  2723  rspc2gv  2732  euind  2800  2reuswapdc  2817  reuind  2818  sbciegft  2867  rspsbc  2919  preqr2g  3606  prel12  3610  intss1  3698  intmin  3703  iinss  3776  disjiun  3832  trel3  3936  trin  3938  trintssmOLD  3945  repizf2  3989  copsexg  4062  po3nr  4128  sowlin  4138  eusvnfb  4267  reusv3  4273  ssorduni  4294  ordsucim  4307  tfis2f  4389  ssrelrel  4526  relop  4574  iss  4745  poirr2  4811  funopg  5034  funssres  5042  funun  5044  funcnvuni  5069  fv3  5312  fvmptt  5378  dff4im  5429  f1eqcocnv  5552  oprabid  5663  f1o2ndf1  5975  poxp  5979  reldmtpos  6000  rntpos  6004  smoiun  6048  tfrlem1  6055  tfrlemi1  6079  tfrexlem  6081  tfri3  6114  nntri3or  6236  qsss  6331  th3qlem1  6374  phplem4  6551  fimax2gtri  6597  fisseneq  6621  sbthlemi10  6654  supmoti  6667  suplub2ti  6675  ordiso2  6707  ltmpig  6877  prcdnql  7022  prcunqu  7023  recexprlem1ssl  7171  recexprlem1ssu  7172  recexprlemss1l  7173  recexprlemss1u  7174  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  caucvgprlemladdrl  7216  mulgt0sr  7302  axprecex  7394  ltxrlt  7531  addid0  7830  negf1o  7839  cju  8393  nngt1ne1  8428  nnsub  8432  0mnnnnn0  8675  un0addcl  8676  un0mulcl  8677  zapne  8791  eluzuzle  8996  indstr  9050  ixxdisj  9290  icodisj  9378  uzsubsubfz  9430  elfzmlbp  9508  fzofzim  9564  subfzo0  9618  addmodlteq  9770  seq3f1olemp  9896  expcl2lemap  9932  expnegzap  9954  expaddzap  9964  expmulzap  9966  facwordi  10113  bccl  10140  hashfacen  10206  ovshftex  10218  cau3lem  10512  maxabslemval  10606  rexanre  10618  2clim  10653  isummo  10737  fsum2dlemstep  10791  fsumiun  10833  odd2np1lem  10965  oddge22np1  10974  sqoddm1div8z  10979  divalglemeunn  11014  divalglemeuneg  11016  gcd0id  11063  divgcdcoprm0  11176  prmdvdsexpr  11222  prmfac1  11224  qnumdencl  11258  hashdvds  11290  bj-vtoclgft  11332  bj-indind  11484  bj-nntrans  11503  bj-nnelirr  11505
  Copyright terms: Public domain W3C validator