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

Theorem syl5bi 151
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 119 . 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 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3imtr4g  204  ancomsd  267  pm2.13dc  853  3jao  1262  19.33b2  1591  sbequ2  1725  sbi1v  1845  mor  2017  2euex  2062  eqneqall  2293  necon3ad  2325  necon1aidc  2334  necon4addc  2353  elnelall  2390  spcimgft  2734  spcimegft  2736  rspc  2755  rspcimdv  2762  rspc2gv  2773  euind  2842  2reuswapdc  2859  reuind  2860  sbciegft  2909  rspsbc  2961  preqr2g  3662  prel12  3666  intss1  3754  intmin  3759  iinss  3832  disjiun  3892  trel3  4002  trin  4004  repizf2  4054  exmidsssnc  4094  copsexg  4134  po3nr  4200  sowlin  4210  eusvnfb  4343  reusv3  4349  ssorduni  4371  ordsucim  4384  tfis2f  4466  ssrelrel  4607  relop  4657  iss  4833  poirr2  4899  funopg  5125  funssres  5133  funun  5135  funcnvuni  5160  fv3  5410  fvmptt  5478  dff4im  5532  f1eqcocnv  5658  oprabid  5769  f1o2ndf1  6091  poxp  6095  reldmtpos  6116  rntpos  6120  smoiun  6164  tfrlem1  6171  tfrlemi1  6195  tfrexlem  6197  tfri3  6230  nntri3or  6355  qsss  6454  th3qlem1  6497  ixpsnf1o  6596  phplem4  6715  fimax2gtri  6761  fiintim  6783  fisseneq  6786  sbthlemi10  6820  supmoti  6846  suplub2ti  6854  ordiso2  6886  ltmpig  7111  prcdnql  7256  prcunqu  7257  recexprlem1ssl  7405  recexprlem1ssu  7406  recexprlemss1l  7407  recexprlemss1u  7408  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgprlemladdrl  7450  mulgt0sr  7550  suplocsrlem  7580  axprecex  7652  ltxrlt  7794  addid0  8099  negf1o  8108  cju  8679  nngt1ne1  8715  nnsub  8719  0mnnnnn0  8963  un0addcl  8964  un0mulcl  8965  zapne  9079  eluzuzle  9286  indstr  9340  xposdif  9616  ixxdisj  9637  icodisj  9726  uzsubsubfz  9778  elfzmlbp  9860  fzofzim  9916  subfzo0  9970  addmodlteq  10122  seq3f1olemp  10226  expcl2lemap  10256  expnegzap  10278  expaddzap  10288  expmulzap  10290  facwordi  10437  bccl  10464  hashfacen  10530  ovshftex  10542  cau3lem  10837  maxabslemval  10931  rexanre  10943  xrmaxiflemval  10970  2clim  11021  summodc  11103  fsum2dlemstep  11154  fsumiun  11197  odd2np1lem  11476  oddge22np1  11485  sqoddm1div8z  11490  divalglemeunn  11525  divalglemeuneg  11527  gcd0id  11574  divgcdcoprm0  11689  prmdvdsexpr  11735  prmfac1  11737  qnumdencl  11771  hashdvds  11803  ctinf  11849  tgcl  12139  epttop  12165  txbas  12333  txbasval  12342  txcnp  12346  txdis1cn  12353  bldisj  12476  reopnap  12613  dvfgg  12732  bj-vtoclgft  12816  bj-indind  12964  bj-nntrans  12983  bj-nnelirr  12985  triap  13058
  Copyright terms: Public domain W3C validator