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

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

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  11379  fprodcom2fi  11567