Theorem pm5.32ri 705

Description: Distribution of implication over biconditional (inference rule).

Hypothesis

Ref	Expression
pm5.32i.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
pm5.32ri	|- ((ps /\ ph) <-> (ch /\ ph))

Proof of Theorem pm5.32ri

Step	Hyp	Ref	Expression
1		pm5.32i.1	. . 3 |- (ph -> (ps <-> ch))
2	1	pm5.32i 704	. 2 |- ((ph /\ ps) <-> (ph /\ ch))
3		ancom 480	. 2 |- ((ps /\ ph) <-> (ph /\ ps))
4		ancom 480	. 2 |- ((ch /\ ph) <-> (ph /\ ch))
5	2, 3, 4	3bitr4i 199	1 |- ((ps /\ ph) <-> (ch /\ ph))

Syntax hints:   -> wi 3   <-> wb 162   /\ wa 239

This theorem is referenced by:  pm5.36 710  2eu5 1694  reuind 2283  rabsn 2916  eufromeq4 3642  dfoprab2 4728  fsplit 4897  th3qlem1 5184  xpsnen 5305  pw2en 5316  rankuni 5618  dfms2 8871  pjimai 11540  isprm2 13567  pm13.193 16057

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

This theorem depends on definitions:  df-bi 163  df-an 241

Copyright terms: Public domain