Theorem bicomi 294

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 243	. 2 |- (ps -> ph)
3	1	biimpi 236	. 2 |- (ph -> ps)
4	2, 3	impbii 235	1 |- (ps <-> ph)

Syntax hints:   <-> wb 231

This theorem is referenced by:  bitr2i 308  bitr3i 309  bitr4i 310  syl5bbr 320  syl5rbbr 322  syl6bbr 326  syl6rbbr 327  3imtr4g 333  mtbir 367  con2bii 395  xor3 424  pm5.41 428  pm4.64 436  pm4.63 438  pm4.61 462  anor 517  ianorOLD 519  pm4.53 522  pm4.55 524  pm4.56 525  pm4.57 527  pm4.25 560  pm4.87 656  pm4.24 722  pm4.77 886  pm4.76 987  pm5.17OLD 1028  pm5.63 1068  3ianor 1142  3oran 1144  pm3.2an3 1327  syl3anbr 1421  3an6 1479  nic-dfim 1539  nic-dfneg 1540  sbid 1857  cleljust 2008  sb10f 2026  nne 2299  necon3bbii 2325  necon2abii 2349  necon2bbii 2350  alexeq 2661  clel2 2667  clel4 2670  sbc8g 2748  cbvralcsf 2852  cbvrexcsf 2853  cbvreucsf 2854  cbvrabcsf 2855  un0 3135  in0 3136  ss0b 3140  opth2 3741  uniuni 3976  eusv2OLD 3995  reusv2 4004  onminex 4063  cotr 4452  dfoprab5sf 5209  oarec 5447  domtriord 5756  isfinite2 5902  en3lplem2 6041  sbc3org 6129  iscard3 6283  cardnum 6284  cardinfima 6286  alephiso 6287  aceqkm 6427  brdom7disj 6454  brdom6disj 6455  grp2grp 10341  ssga 10476  hausfillim 11299  lejdii 12086  nmcopexlem1 12578  nmcfnexlem1 12607  mdslle1i 12878  mdslle2i 12879  mdslj1i 12880  mdslj2i 12881  bnj208 13033  bnj184 13035  bnj445 13261  bnj456 13272  bnj467 13283  bnj490 13305  bnj1 13327  bnj3 13329  bnj24 13345  bnj38 13360  bnj43 13364  bnj51 13372  bnj112 13397  bnj115 13399  bnj156 13420  bnj205 13433  bnj612 13494  bnj613 13495  bnj856 13718  bnj858 13720  bnj861 13723  bnj947 13775  bnj971 13789  bnj979 13792  bnj1048 13817  bnj1392 14035  bnj1393 14036  bnj1473 14077  bnj119 14158  bnj121 14160  bnj124 14163  bnj130 14169  bnj153 14176  bnj207 14177  bnj606 14222  bnj581 14223  bnj607 14233  bnj611 14236  bnj965 14275  bnj1000 14293  bnj1040 14317  bnj1049 14323  bnj1070 14330  bnj1134 14356  3an6OLD 14681  dfso2 14711  fundmpss 14714  TFIid 15062  TNid 15065  TTBid 15067  FFBid 15070  nabi1i 15088  nabi2i 15089  negcmpprcal2 15237  vutr 15246  boxeq 15283  notev 15285  notal 15286  albineal 15292  splint 15321  ficli 15324  restidsing 15362  imfstnrelc 15368  omslim 15393  rngop 15479  fopab2g 15480  defse3 15614  qusp 15932  eltpt 15933  rcfpfillem3 15957  limfillem1 15965  grphm 16035  cntrsetlem 16052  algi 16129  dualcat2lem 16184  dualded2lem 16185  dualded 16187  settrcon 16318  tarval2 16320  vtarsuelt 16343  dmsdtriordOLD 16445  trer 16446  alexsublem3 16524  locfindsc 16600  inixp 16807  eropreu 16818  firnfi3 16828  geomcau 16934  lmclim2 16935  heiborlem24 17063  an43 17320  pm10.252 17392  pm10.253 17393  pm10.42 17396  2nexaln 17412  aaanv 17430  pm13.195 17462  2sbc6g 17464  2sbc5g 17465  cbvralcsfOLD 17496  cbvrexcsfOLD 17497  cbvreucsfOLD 17498  cbvrabcsfOLD 17499  en3lpVD 17764  3orbi123VD 17769  sbc3orgVD 17770  undif3VD 17801  isopos 17837  islvol5 18283  elpadd0 18513  osumcllem11 18651  pexmidlem8 18662

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 232

Copyright terms: Public domain