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  794  baib  827  pm5.6dc  834  xornbidc  1279  mo2dc  1952  reu8  2731  sbc6g  2782  r19.28m  3305  r19.45mv  3309  r19.27m  3310  ralsns  3399  rexsnsOLD  3401  iunconstm  3656  iinconstm  3657  unisucg  4117  funssres  4885  fncnv  4908  dff1o5  5078  funimass4  5167  fneqeql2  5219  fnniniseg2  5233  rexsupp  5234  unpreima  5235  dffo3  5257  funfvima  5333  dff13  5350  f1eqcocnv  5374  fliftf  5382  isocnv2  5395  eloprabga  5533  mpt22eqb  5552  opabex3d  5690  opabex3  5691  elxp6  5738  elxp7  5739  genpdflem  6490  ltexprlemloc  6581  xrlenlt  6881  negcon2  7060  elznn  8037  zq  8337  rpnegap  8390
  Copyright terms: Public domain W3C validator