ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylbbr Unicode version

Theorem sylbbr 135
Description: A mixed syllogism inference from two biconditionals.

Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 14 infers an implication from two implications (and there are 3syl 17 and 4syl 18 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 120, sylib 121, sylbir 134, sylibr 133; four inferences inferring an implication from two biconditionals: sylbb 122, sylbbr 135, sylbb1 136, sylbb2 137; four inferences inferring a biconditional from two biconditionals: bitri 183, bitr2i 184, bitr3i 185, bitr4i 186 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 45, syl5 32, syl6 33, mpbid 146, bitrd 187, syl5bb 191, bitrdi 195 and variants. (Contributed by BJ, 21-Apr-2019.)

Hypotheses
Ref Expression
sylbbr.1  |-  ( ph  <->  ps )
sylbbr.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
sylbbr  |-  ( ch 
->  ph )

Proof of Theorem sylbbr
StepHypRef Expression
1 sylbbr.2 . . 3  |-  ( ps  <->  ch )
21biimpri 132 . 2  |-  ( ch 
->  ps )
3 sylbbr.1 . 2  |-  ( ph  <->  ps )
42, 3sylibr 133 1  |-  ( ch 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  fisumcom2  11373  fprodcom2fi  11561
  Copyright terms: Public domain W3C validator