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  813  3jao  1233  19.33b2  1561  sbequ2  1693  sbi1v  1813  mor  1984  2euex  2029  eqneqall  2256  necon3ad  2288  necon1aidc  2297  necon4addc  2316  spcimgft  2675  spcimegft  2677  rspc  2696  rspcimdv  2703  rspc2gv  2713  euind  2780  2reuswapdc  2795  reuind  2796  sbciegft  2845  rspsbc  2897  preqr2g  3567  prel12  3571  intss1  3659  intmin  3664  iinss  3737  trel3  3891  trin  3893  trintssmOLD  3900  repizf2  3944  copsexg  4007  po3nr  4073  sowlin  4083  eusvnfb  4212  reusv3  4218  ssorduni  4239  ordsucim  4252  tfis2f  4333  ssrelrel  4466  relop  4514  iss  4684  poirr2  4747  funopg  4964  funssres  4972  funun  4974  funcnvuni  4999  fv3  5229  fvmptt  5294  dff4im  5345  f1eqcocnv  5462  oprabid  5568  f1o2ndf1  5880  poxp  5884  reldmtpos  5902  rntpos  5906  smoiun  5950  tfrlem1  5957  tfrlemi1  5981  tfrexlem  5983  tfri3  6016  nntri3or  6137  qsss  6231  th3qlem1  6274  phplem4  6390  supmoti  6465  suplub2ti  6473  ordiso2  6505  ltmpig  6591  prcdnql  6736  prcunqu  6737  recexprlem1ssl  6885  recexprlem1ssu  6886  recexprlemss1l  6887  recexprlemss1u  6888  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  caucvgprlemladdrl  6930  mulgt0sr  7016  axprecex  7108  ltxrlt  7245  addid0  7544  negf1o  7553  cju  8105  nngt1ne1  8140  nnsub  8144  0mnnnnn0  8387  un0addcl  8388  un0mulcl  8389  zapne  8503  eluzuzle  8708  indstr  8762  ixxdisj  9002  icodisj  9090  uzsubsubfz  9142  elfzmlbp  9220  fzofzim  9274  subfzo0  9328  addmodlteq  9480  expcl2lemap  9585  expnegzap  9607  expaddzap  9617  expmulzap  9619  facwordi  9764  bccl  9791  ovshftex  9845  cau3lem  10138  maxabslemval  10232  rexanre  10244  2clim  10278  odd2np1lem  10416  oddge22np1  10425  sqoddm1div8z  10430  divalglemeunn  10465  divalglemeuneg  10467  gcd0id  10514  divgcdcoprm0  10627  prmdvdsexpr  10673  prmfac1  10675  bj-vtoclgft  10736  bj-indind  10885  bj-nntrans  10904  bj-nnelirr  10906
  Copyright terms: Public domain W3C validator