Theorem bicomi 189

Description: Inference from commutative law for logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem bicomi

Step	Hyp	Ref	Expression
1		bicomi.1	. . 3 |- (ph <-> ps)
2	1	biimpri 169	. 2 |- (ps -> ph)
3	1	biimpi 168	. 2 |- (ph -> ps)
4	2, 3	impbii 174	1 |- (ps <-> ph)

Syntax hints:   <-> wb 163

This theorem is referenced by:  bitr2i 191  bitr3i 192  bitr4i 193  con2bii 238  pm4.64 243  pm4.63 245  pm4.61 258  pm4.25 264  ianor 329  pm4.53 334  pm4.55 336  pm4.56 337  pm4.57 340  pm4.87 383  pm4.77 468  pm4.24 479  syl5bbr 593  syl5rbbr 594  syl6bbr 597  syl6rbbr 598  3imtr4g 612  pm4.76 660  pm5.17 731  xor3 737  3ianor 870  pm3.2an3 1049  syl3anbr 1141  nic-dfim 1235  nic-dfneg 1236  ee3bir 1274  sbid 1549  cleljust 1713  sb10f 1733  nne 2021  necon3bbii 2031  necon2abii 2063  necon2bbii 2064  alexeq 2390  clel2 2396  clel4 2399  sbc8g 2477  difeqriOLD 2728  un0 2896  in0 2897  ss0b 2901  brab1OLD 3385  opth2 3546  uniuni 3806  euexeqOLD 3826  euexaleq 3827  onminex 3888  cotr 4302  dfoprab5sf 5058  oarec 5244  domtriord 5546  isfinite2 5639  sbc3org 5827  aceqkm 5943  brdom7disj 5966  brdom6disj 5967  iscard3 6036  cardnum 6037  cardinfima 6039  alephiso 6040  ltxr 6664  ssga 9455  hausfillim 10303  lejdii 11094  nmcopexlem1 11588  nmcfnexlem1 11617  mdslle1i 11889  mdslle2i 11890  mdslj1i 11891  mdslj2i 11892  bnj208 12051  bnj184 12054  bnj445 12294  bnj456 12306  bnj467 12318  bnj490 12342  bnj1 12366  bnj3 12368  bnj24 12388  bnj33OLD 12402  bnj38 12409  bnj43 12414  bnj51 12426  bnj112 12457  bnj115 12459  bnj156 12482  bnj205 12498  bnj612 12565  bnj613 12566  bnj856 12789  bnj858 12791  bnj861 12794  bnj947 12846  bnj971 12860  bnj979 12863  bnj1048 12888  bnj1392 13106  bnj1393 13107  bnj1473 13148  bnj119 13229  bnj121 13231  bnj124 13234  bnj130 13240  bnj153 13247  bnj207 13248  bnj606 13293  bnj581 13294  bnj607 13304  bnj611 13307  bnj965 13346  bnj1000 13364  bnj1040 13388  bnj1049 13394  bnj1070 13401  bnj1134 13427  3an6 13803  fundmpss 13836  TFIid 14115  TNid 14118  TTBid 14120  FFBid 14123  nabi1i 14141  nabi2i 14142  negcmpprcal2 14276  vutr 14285  boxeq 14314  notev 14316  notal 14317  albineal 14323  ficli 14353  restidsing 14391  imfstnrelc 14396  omslim 14420  rngop 14484  fopab2g 14485  defse3 14614  qusp 14908  eltpt 14909  rcfpfillem3 14930  limfillem1 14938  cntrsetlem 14999  algi 15074  dualcat2lem 15129  dualded2lem 15130  dualded 15132  settrcon 15247  tarval2 15249  vtarsuelt 15272  dmsdtriordOLD 15360  trer 15361  alexsublem3 15439  locfindsc 15515  cnpfillim 15589  inixp 15722  eropreu 15733  firnfi3 15743  geomcau 15849  lmclim2 15850  heiborlem24 15978  an43 16235  pm10.252 16307  pm10.253 16308  pm10.42 16311  2nexaln 16327  aaanv 16345  pm13.195 16377  2sbc6g 16379  2sbc5g 16380  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  en3lpVD 16669  3orbi123VD 16674  sbc3orgVD 16675  undif3VD 16706  islvec 17188  elpadd0 17270  osumcllem11 17374  pexmidlem8 17385

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 164

Copyright terms: Public domain