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

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3 (𝜑𝜓)
21biimpi 119 . 2 (𝜑𝜓)
3 syl5bi.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 32 1 (𝜒 → (𝜑𝜃))
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  870  3jao  1279  19.33b2  1608  sbequ2  1742  sbi1v  1863  mor  2041  2euex  2086  eqneqall  2318  necon3ad  2350  necon1aidc  2359  necon4addc  2378  elnelall  2415  spcimgft  2762  spcimegft  2764  rspc  2783  rspcimdv  2790  rspc2gv  2801  euind  2871  2reuswapdc  2888  reuind  2889  sbciegft  2939  rspsbc  2991  preqr2g  3694  prel12  3698  intss1  3786  intmin  3791  iinss  3864  disjiun  3924  trel3  4034  trin  4036  repizf2  4086  exmidsssnc  4126  copsexg  4166  po3nr  4232  sowlin  4242  eusvnfb  4375  reusv3  4381  ssorduni  4403  ordsucim  4416  tfis2f  4498  ssrelrel  4639  relop  4689  iss  4865  poirr2  4931  funopg  5157  funssres  5165  funun  5167  funcnvuni  5192  fv3  5444  fvmptt  5512  dff4im  5566  f1eqcocnv  5692  oprabid  5803  f1o2ndf1  6125  poxp  6129  reldmtpos  6150  rntpos  6154  smoiun  6198  tfrlem1  6205  tfrlemi1  6229  tfrexlem  6231  tfri3  6264  nntri3or  6389  qsss  6488  th3qlem1  6531  ixpsnf1o  6630  phplem4  6749  fimax2gtri  6795  fiintim  6817  fisseneq  6820  sbthlemi10  6854  supmoti  6880  suplub2ti  6888  ordiso2  6920  ltmpig  7154  prcdnql  7299  prcunqu  7300  recexprlem1ssl  7448  recexprlem1ssu  7449  recexprlemss1l  7450  recexprlemss1u  7451  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  caucvgprlemladdrl  7493  mulgt0sr  7593  suplocsrlem  7623  axprecex  7695  ltxrlt  7837  addid0  8142  negf1o  8151  cju  8726  nngt1ne1  8762  nnsub  8766  0mnnnnn0  9016  un0addcl  9017  un0mulcl  9018  zapne  9132  eluzuzle  9341  indstr  9395  xposdif  9672  ixxdisj  9693  icodisj  9782  uzsubsubfz  9834  elfzmlbp  9916  fzofzim  9972  subfzo0  10026  addmodlteq  10178  seq3f1olemp  10282  expcl2lemap  10312  expnegzap  10334  expaddzap  10344  expmulzap  10346  facwordi  10493  bccl  10520  hashfacen  10586  ovshftex  10598  cau3lem  10893  maxabslemval  10987  rexanre  10999  xrmaxiflemval  11026  2clim  11077  summodc  11159  fsum2dlemstep  11210  fsumiun  11253  prodmodc  11354  odd2np1lem  11576  oddge22np1  11585  sqoddm1div8z  11590  divalglemeunn  11625  divalglemeuneg  11627  gcd0id  11674  divgcdcoprm0  11789  prmdvdsexpr  11835  prmfac1  11837  qnumdencl  11872  hashdvds  11904  ctinf  11950  tgcl  12243  epttop  12269  txbas  12437  txbasval  12446  txcnp  12450  txdis1cn  12457  bldisj  12580  reopnap  12717  dvfgg  12836  bj-vtoclgft  13012  bj-indind  13160  bj-nntrans  13179  bj-nnelirr  13181  triap  13254
  Copyright terms: Public domain W3C validator