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

Theorem sylbbr 136
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 121, sylib 122, sylbir 135, sylibr 134; four inferences inferring an implication from two biconditionals: sylbb 123, sylbbr 136, sylbb1 137, sylbb2 138; four inferences inferring a biconditional from two biconditionals: bitri 184, bitr2i 185, bitr3i 186, bitr4i 187 (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 147, bitrd 188, bitrid 192, bitrdi 196 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 133 . 2  |-  ( ch 
->  ps )
3 sylbbr.1 . 2  |-  ( ph  <->  ps )
42, 3sylibr 134 1  |-  ( ch 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  fisumcom2  11413  fprodcom2fi  11601
  Copyright terms: Public domain W3C validator