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  612  limelon  4102  eldifpw  4174  ssonuni  4180  peano2  4261  limom  4279  elrnmpt1  4528  cnveqb  4719  cnveq0  4720  relcoi1  4792  ndmfvg  5147  ffvresb  5271  caovord3d  5613  poxp  5794  nnm0r  5997  nnacl  5998  nnacom  6002  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  nnmcom  6007  brecop  6132  ecopovtrn  6139  ecopovtrng  6142  fundmen  6222  mulcmpblnq  6352  ordpipqqs  6358  mulcmpblnq0  6426  genpprecll  6496  genppreclu  6497  addcmpblnr  6627  ax1rid  6721  axpre-mulgt0  6731  cnegexlem1  6943  msqge0  7360  mulge0  7363  ltleap  7373  nnmulcl  7676  nnsub  7693  elnn0z  7994  ztri3or0  8023  nneoor  8076  uz11  8231  xltnegi  8478  frec2uzuzd  8829  iseqfveq2  8865  m1expcl2  8891  expadd  8911  expmul  8914  bj-om  9325  peano5set  9328  bj-inf2vnlem2  9355  bj-inf2vn  9358  bj-inf2vn2  9359
  Copyright terms: Public domain W3C validator