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

Theorem syl5bi 141
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 113 . 2 (φψ)
3 syl5bi.2 . 2 (χ → (ψθ))
42, 3syl5 28 1 (χ → (φθ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr4g  194  ancomsd  256  pm2.13dc  778  3jao  1195  19.33b2  1517  sbequ2  1649  sbi1v  1768  mor  1939  2euex  1984  necon3ad  2241  necon1aidc  2250  necon4addc  2269  spcimgft  2623  spcimegft  2625  rspc  2644  rspcimdv  2651  euind  2722  2reuswapdc  2737  reuind  2738  sbciegft  2787  rspsbc  2834  preqr2g  3529  prel12  3533  intss1  3621  intmin  3626  iinss  3699  trel3  3853  trin  3855  trintssm  3861  repizf2  3906  copsexg  3972  po3nr  4038  sowlin  4048  eusvnfb  4152  reusv3  4158  ssorduni  4179  ordsucim  4192  tfis2f  4250  ssrelrel  4383  relop  4429  iss  4597  poirr2  4660  funopg  4877  funssres  4885  funun  4887  funcnvuni  4911  fv3  5140  fvmptt  5205  dff4im  5256  f1eqcocnv  5374  oprabid  5480  f1o2ndf1  5791  poxp  5794  reldmtpos  5809  rntpos  5813  smoiun  5857  tfrlem1  5864  tfrlemi1  5887  tfrexlem  5889  tfri3  5894  rdgon  5913  nntri3or  6011  qsss  6101  th3qlem1  6144  ltmpig  6323  prcdnql  6466  prcunqu  6467  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1l  6606  recexprlemss1u  6607  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  mulgt0sr  6684  axprecex  6744  ltxrlt  6862  cju  7674  nngt1ne1  7709  nnsub  7713  0mnnnnn0  7970  un0addcl  7971  un0mulcl  7972  zapne  8071  eluzuzle  8237  indstr  8292  ixxdisj  8522  icodisj  8610  uzsubsubfz  8661  elfzmlbp  8740  fzofzim  8794  expcl2lemap  8901  expnegzap  8923  expaddzap  8933  expmulzap  8935  bj-vtoclgft  9229  bj-nntrans  9385  bj-nnelirr  9387
  Copyright terms: Public domain W3C validator