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

Theorem syl6rbbr 188
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl6rbbr.1 (φ → (ψχ))
syl6rbbr.2 (θχ)
Assertion
Ref Expression
syl6rbbr (φ → (θψ))

Proof of Theorem syl6rbbr
StepHypRef Expression
1 syl6rbbr.1 . 2 (φ → (ψχ))
2 syl6rbbr.2 . . 3 (θχ)
32bicomi 123 . 2 (χθ)
41, 3syl6rbb 186 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:  imimorbdc  779  baib  812  pm5.6dc  817  xornbidc  1260  mo2dc  1928  reu8  2705  sbc6g  2756  r19.28m  3279  r19.45mv  3283  r19.27m  3284  ralsns  3371  rexsnsOLD  3373  iunconstm  3628  iinconstm  3629  unisucg  4089  funssres  4856  fncnv  4879  dff1o5  5048  funimass4  5137  fneqeql2  5189  fnniniseg2  5203  rexsupp  5204  unpreima  5205  dffo3  5227  funfvima  5303  dff13  5320  f1eqcocnv  5344  fliftf  5352  isocnv2  5365  eloprabga  5502  mpt22eqb  5521  opabex3d  5659  opabex3  5660  elxp6  5707  elxp7  5708  genpdflem  6347  ltexprlemloc  6430  xrlenlt  6684  negcon2  6863  elznn  7835  zq  8043  rpnegap  8095
  Copyright terms: Public domain W3C validator