NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl5ib GIF version

Theorem syl5ib 210
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5ib.1 (φψ)
syl5ib.2 (χ → (ψθ))
Assertion
Ref Expression
syl5ib (χ → (φθ))

Proof of Theorem syl5ib
StepHypRef Expression
1 syl5ib.1 . 2 (φψ)
2 syl5ib.2 . . 3 (χ → (ψθ))
32biimpd 198 . 2 (χ → (ψθ))
41, 3syl5 28 1 (χ → (φθ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  syl5ibcom  211  syl5ibr  212  19.23tOLD  1819  nfsb4t  2080  ax11indalem  2197  ax11inda2ALT  2198  gencl  2887  spsbc  3058  eqsbc3r  3103  ssnelpss  3613  adj11  3889  uniintsn  3963  phi011lem1  4598  optocl  4838  xpexr  5109  funimass1  5169  fneu  5187  dmfex  5247  fniniseg  5371  eqfnfv  5392  eqfnfv2  5393  elpreima  5407  fnasrn  5417  dffo4  5423  fconst5  5455  funiunfv  5467  dff13  5471  f1ocnvfv  5478  f1ocnvfvb  5479  ce0ncpw1  6185  cecl  6186  dflec3  6221  lenc  6223
  Copyright terms: Public domain W3C validator