Theorem baibr 686

Description: Move conjunction outside of biconditional.

Hypothesis

Ref	Expression
baibr.1	|- (ph <-> (ps /\ ch))

Assertion

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

Proof of Theorem baibr

Step	Hyp	Ref	Expression
1		baibr.1	. . 3 |- (ph <-> (ps /\ ch))
2	1	baib 685	. 2 |- (ps -> (ph <-> ch))
3	2	bicomd 521	1 |- (ps -> (ch <-> ph))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  pm5.44 687  exmoeu2 1414  ssnelpss 2330  reuunixfr 2906  brinxp 3232  canth 3907  kmlem14 4778  iscard 4853  elioo5t 6384  islp2 7747  adjeqt 9859  lnopcnbdt 9965  cvexchlem 10295

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 147  df-an 225

Copyright terms: Public domain