Theorem bicomi 172

Description: Inference from commutative law for logical equivalence.

Hypothesis

Ref	Expression
bicom.1	|- (ph <-> ps)

Assertion

Ref	Expression
bicomi	|- (ps <-> ph)

Proof of Theorem bicomi

Step	Hyp	Ref	Expression
1		bicom.1	. . 3 |- (ph <-> ps)
2	1	biimpr 152	. 2 |- (ps -> ph)
3	1	biimp 151	. 2 |- (ph -> ps)
4	2, 3	impbi 157	1 |- (ps <-> ph)

Syntax hints:   <-> wb 146

This theorem is referenced by:  bitr2 174  bitr3 175  bitr4 176  con2bii 221  pm4.64 226  pm4.63 228  pm4.61 239  pm4.25 244  pm4.53 308  pm4.55 310  pm4.56 311  pm4.57 313  pm4.87 356  pm4.77 423  pm4.24 433  syl5bbr 534  syl5rbbr 535  syl6bbr 538  syl6rbbr 539  3imtr4g 553  pm4.76 599  pm5.17 668  xor3 674  sbid 1184  cleljust 1328  sb10f 1342  nne 1589  necon3bbii 1597  necon2abii 1620  necon2bbii 1621  alexeq 1885  clel2 1891  clel4 1894  difeqri 2160  un0 2297  in0 2298  ss0b 2302  brab1 2660  opth2 2800  uniuni 2880  onminex 3020  oarec 4196  isfinite2OLD 4546  aceqkm 4781  brdom7disj 4804  brdom6disj 4805  iscard3 4888  cardnum 4889  cardinfima 4891  alephiso 4892  ltxrt 5495  lejdi 9461  nmcopexlem1 9951  nmcfnexlem1 9980  mdslle1 10244  mdslle2 10245  mdslj1 10246  mdslj2 10247  ficli 10472  ficliOLD 10473  qusp 10555  rcfpfillem3 10589  rcfpfillem3OLD 10590  sfvlim 10605  algi 10660

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

Copyright terms: Public domain