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  6603  recexprlem1ssu  6604  recexprlemss1l  6605  recexprlemss1u  6606  mulgt0sr  6664  axprecex  6724  ltxrlt  6842  cju  7654  nngt1ne1  7689  nnsub  7693  0mnnnnn0  7950  un0addcl  7951  un0mulcl  7952  zapne  8051  eluzuzle  8217  indstr  8272  ixxdisj  8502  icodisj  8590  uzsubsubfz  8641  elfzmlbp  8720  fzofzim  8774  expcl2lemap  8881  expnegzap  8903  expaddzap  8913  expmulzap  8915  bj-vtoclgft  9183  bj-nntrans  9339  bj-nnelirr  9341
  Copyright terms: Public domain W3C validator