Theorem bicomi 150

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 134	. 2 |- (ps -> ph)
3	1	biimp 133	. 2 |- (ph -> ps)
4	2, 3	impbi 139	1 |- (ps <-> ph)

Syntax hints:   <-> wb 127

This theorem is referenced by:  bitr2 152  bitr3 153  bitr4 154  bicon2i 194  syl5bbr 412  syl5rbbr 413  syl6bbr 416  syl6rbbr 417  3imtr4g 426  pm5.74 442  sbid 868  cleljust 985  sb5 988  sb6 989  euanv 1053  exists1 1072  sbabel 1189  clel2 1374  clel3 1375  clel4 1376  sbc6 1453  difeqri 1589  un0 1721  in0 1722  disj1 1734  opth2 1909  dftr3 2045  brab1 2096  onminex 2275  snec 3232  isfinite2 3437  aceq2 3554  kmlem13 3592  iscard3 3693  cardnum 3694  cardinfima 3696  alephiso 3697  cardcf 3706  sup3 4511  hoeq 5595  atom1d 5750

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

This theorem depends on definitions:  df-bi 128

metamath.org