ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5bi GIF 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 (𝜑𝜓)
syl5bi.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bi (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3 (𝜑𝜓)
21biimpi 118 . 2 (𝜑𝜓)
3 syl5bi.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 32 1 (𝜒 → (𝜑𝜃))
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  3561  prel12  3565  intss1  3653  intmin  3658  iinss  3731  trel3  3885  trin  3887  trintssmOLD  3894  repizf2  3938  copsexg  4001  po3nr  4067  sowlin  4077  eusvnfb  4206  reusv3  4212  ssorduni  4233  ordsucim  4246  tfis2f  4327  ssrelrel  4460  relop  4508  iss  4678  poirr2  4741  funopg  4958  funssres  4966  funun  4968  funcnvuni  4993  fv3  5223  fvmptt  5288  dff4im  5339  f1eqcocnv  5456  oprabid  5562  f1o2ndf1  5874  poxp  5878  reldmtpos  5896  rntpos  5900  smoiun  5944  tfrlem1  5951  tfrlemi1  5975  tfrexlem  5977  tfri3  6010  nntri3or  6130  qsss  6224  th3qlem1  6267  phplem4  6380  supmoti  6455  suplub2ti  6463  ordiso2  6495  ltmpig  6580  prcdnql  6725  prcunqu  6726  recexprlem1ssl  6874  recexprlem1ssu  6875  recexprlemss1l  6876  recexprlemss1u  6877  cauappcvgprlemladdru  6897  cauappcvgprlemladdrl  6898  caucvgprlemladdrl  6919  mulgt0sr  7005  axprecex  7097  ltxrlt  7234  addid0  7533  negf1o  7542  cju  8094  nngt1ne1  8129  nnsub  8133  0mnnnnn0  8376  un0addcl  8377  un0mulcl  8378  zapne  8492  eluzuzle  8697  indstr  8751  ixxdisj  8991  icodisj  9079  uzsubsubfz  9131  elfzmlbp  9209  fzofzim  9263  subfzo0  9317  addmodlteq  9469  expcl2lemap  9574  expnegzap  9596  expaddzap  9606  expmulzap  9608  facwordi  9753  bccl  9780  ovshftex  9834  cau3lem  10127  maxabslemval  10221  rexanre  10233  2clim  10267  odd2np1lem  10405  oddge22np1  10414  sqoddm1div8z  10419  divalglemeunn  10454  divalglemeuneg  10456  gcd0id  10503  divgcdcoprm0  10616  prmdvdsexpr  10662  prmfac1  10664  bj-vtoclgft  10721  bj-indind  10870  bj-nntrans  10889  bj-nnelirr  10891
  Copyright terms: Public domain W3C validator