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

Theorem syl5ibr 145
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.)
Hypotheses
Ref Expression
syl5ibr.1 (φθ)
syl5ibr.2 (χ → (ψθ))
Assertion
Ref Expression
syl5ibr (χ → (φψ))

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2 (φθ)
2 syl5ibr.2 . . 3 (χ → (ψθ))
32bicomd 129 . 2 (χ → (θψ))
41, 3syl5ib 143 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  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  syl5ibrcom  146  biimprd  147  nbn2  600  limelon  4081  eldifpw  4154  ssonuni  4160  peano2  4241  limom  4259  elrnmpt1  4508  cnveqb  4699  cnveq0  4700  relcoi1  4772  ndmfvg  5125  ffvresb  5249  caovord3d  5590  poxp  5771  frec0g  5898  nnm0r  5969  nnacl  5970  nnacom  5974  nnaass  5975  nndi  5976  nnmass  5977  nnmsucr  5978  nnmcom  5979  brecop  6103  ecopovtrn  6110  ecopovtrng  6113  mulcmpblnq  6221  ordpipqqs  6227  mulcmpblnq0  6293  genpprecll  6362  genppreclu  6363  addcmpblnr  6483  ax1rid  6570  axpre-mulgt0  6580  cnegexlem1  6788  bj-om  7355  peano5set  7358  bj-inf2vnlem2  7385  bj-inf2vn  7388  bj-inf2vn2  7389
  Copyright terms: Public domain W3C validator