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  772  3jao  1182  19.33b2  1502  sbequ2  1634  sbi1v  1753  mor  1924  2euex  1969  necon3ad  2225  necon1aidc  2234  necon4addc  2253  spcimgft  2606  spcimegft  2608  rspc  2627  rspcimdv  2634  euind  2705  2reuswapdc  2720  reuind  2721  sbciegft  2770  rspsbc  2817  preqr2g  3512  prel12  3516  intss1  3604  intmin  3609  iinss  3682  trel3  3836  trin  3838  trintssm  3844  repizf2  3889  copsexg  3955  po3nr  4021  sowlin  4031  eusvnfb  4136  reusv3  4142  ssorduni  4163  ordsucim  4176  tfis2f  4234  ssrelrel  4367  relop  4413  iss  4581  poirr2  4644  funopg  4860  funssres  4868  funun  4870  funcnvuni  4894  fv3  5122  fvmptt  5187  dff4im  5238  f1eqcocnv  5356  oprabid  5461  f1o2ndf1  5772  poxp  5775  reldmtpos  5790  rntpos  5794  smoiun  5838  tfrlem1  5845  tfrlemi1  5867  tfrexlem  5870  tfri3  5875  rdgon  5893  nntri3or  5987  qsss  6076  th3qlem1  6119  ltmpig  6199  prcdnql  6338  prcunqu  6339  recexprlem1ssl  6467  recexprlem1ssu  6468  recexprlemss1l  6469  recexprlemss1u  6470  mulgt0sr  6522  axprecex  6574  ltxrlt  6686  bj-vtoclgft  7021  bj-nntrans  7173  bj-nnelirr  7175
  Copyright terms: Public domain W3C validator