Theorem sylbbr 134

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 119, sylib 120, sylbir 133, sylibr 132; four inferences inferring an implication from two biconditionals: sylbb 121, sylbbr 134, sylbb1 135, sylbb2 136; four inferences inferring a biconditional from two biconditionals: bitri 182, bitr2i 183, bitr3i 184, bitr4i 185 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 44, syl5 32, syl6 33, mpbid 145, bitrd 186, syl5bb 190, syl6bb 194 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

Step	Hyp	Ref	Expression
1		sylbbr.2	. . 3 |- ( ps <-> ch )
2	1	biimpri 131	. 2 |- ( ch -> ps )
3		sylbbr.1	. 2 |- ( ph <-> ps )
4	2, 3	sylibr 132	1 |- ( ch -> ph )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by: (None)