Theorem baib 685

Description: Move conjunction outside of biconditional.

Hypothesis

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

Assertion

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

Proof of Theorem baib

Step	Hyp	Ref	Expression
1		ibar 643	. 2 |- (ps -> (ch <-> (ps /\ ch)))
2		baib.1	. 2 |- (ph <-> (ps /\ ch))
3	1, 2	syl6rbbr 539	1 |- (ps -> (ph <-> ch))

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

This theorem is referenced by:  baibr 686  elrab3 1906  elabsg 1965  rabsn 2445  reuunixfr 2906  nlimon 3122  ltresr 5258  xrlenltt 5501  znnnlt1t 6156  nn0subt 6161  elfzt 6471  lmss 7953  seq1hcau 9054  sh2 9091  adjvalt 9814  lnopcnret 9968  dmdbr2 10230  elatcv0 10268  ahypfmbi 10426

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