Theorem baibr 945

Description: Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)

Hypothesis

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

Assertion

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

Proof of Theorem baibr

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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  df-an 386

This theorem is referenced by:  pm5.44  950  exmoeu2  2497  ssnelpss  3718  brinxp  5181  copsex2ga  5231  canth  6608  riotaxfrd  6642  iscard  8801  kmlem14  8985  ltxrlt  10108  elioo5  12231  prmind2  15398  pcelnn  15574  isnirred  18700  isreg2  21181  comppfsc  21335  kqcldsat  21536  elmptrab  21630  itg2uba  23510  prmorcht  24904  adjeq  28794  lnopcnbd  28895  cvexchlem  29227  maprnin  29506  topfne  32349  ismblfin  33450  ftc1anclem5  33489  isdmn2  33854  cdlemefrs29pre00  35683  cdlemefrs29cpre1  35686  isdomn3  37782  elmapintab  37902  bits0ALTV  41590