Theorem bija 370

Description: Combine antecedents into a single biconditional. This inference, reminiscent of ja 173, is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im 253 and pm5.21im 364). (Contributed by Wolf Lammen, 13-May-2013.)

Hypotheses

Ref	Expression
bija.1	|- ( ph -> ( ps -> ch ) )
bija.2	|- ( -. ph -> ( -. ps -> ch ) )

Assertion

Ref	Expression
bija	|- ( ( ph <-> ps ) -> ch )

Proof of Theorem bija

Step	Hyp	Ref	Expression
1		biimpr 210	. . 3 |- ( ( ph <-> ps ) -> ( ps -> ph ) )
2		bija.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	syli 39	. 2 |- ( ( ph <-> ps ) -> ( ps -> ch ) )
4		biimp 205	. . . 4 |- ( ( ph <-> ps ) -> ( ph -> ps ) )
5	4	con3d 148	. . 3 |- ( ( ph <-> ps ) -> ( -. ps -> -. ph ) )
6		bija.2	. . 3 |- ( -. ph -> ( -. ps -> ch ) )
7	5, 6	syli 39	. 2 |- ( ( ph <-> ps ) -> ( -. ps -> ch ) )
8	3, 7	pm2.61d 170	1 |- ( ( ph <-> ps ) -> ch )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  equvel  2347  2lgsoddprm  25141  bj-bibibi  32571  wl-aleq  33322  wl-nfeqfb  33323  rp-fakeimass  37857  rp-fakenanass  37860