Theorem bicomd 580

Description: Commute two sides of a biconditional in a deduction.

Hypothesis

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

Assertion

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

Proof of Theorem bicomd

Step	Hyp	Ref	Expression
1		bicomd.1	. 2 |- (ph -> (ps <-> ch))
2		bicom 579	. 2 |- ((ps <-> ch) <-> (ch <-> ps))
3	1, 2	sylib 215	1 |- (ph -> (ch <-> ps))

Syntax hints:   -> wi 3   <-> wb 163

This theorem is referenced by:  con1bid 586  bitr2d 588  bitr3d 589  bitr4d 590  syl5rbb 592  syl6rbb 596  ibir 653  pm5.54 747  baibr 750  pm5.5 804  bimsc1 823  ninba 847  bitr3 1283  sbequ12r 1546  sbco 1625  sbidmOLD 1628  sbco2 1629  necon3bbid 2034  ralcom2 2244  gencbvex 2334  gencbvexOLD 2335  clel3g 2397  cbvab 2419  moi2 2435  moi 2436  reu8 2448  sbhypf 2452  sbcco2 2468  r19.9rzv 2963  ifboth 3002  sbcsng 3086  iununi 3331  iununiOLD 3332  opabid 3557  poeq2 3595  posn 3603  soeq2 3609  freq2 3633  tfinds2 3947  fconstfv 4825  isoid 4872  isoini 4877  isowe 4880  f1oweALT 4883  tfrlem5 5123  oawordOLD 5231  oalimcl 5242  omword 5249  oeword 5265  nnaordex 5306  nnawordex 5307  pw2en 5505  ordiso 5683  omsubsdom 5881  carduni 6010  aleph11 6027  alephval3 6051  axrepndlem2 6097  lttri2 6682  xrlttri2 6730  mulne0bOLD 6886  lemul1 7011  lemul1OLD 7012  lt2msqi 7064  msq11i 7066  nn0ind-raph 7426  zindd 7427  rebtwnz 7435  qreccl 7453  qsqueeze 7461  iooshf 7564  om2uzlti 7709  2climnn 8362  2climnn0 8363  ef01tllem2OLD 8647  znnen 8771  gch-kn 8856  bastop1 8912  iscld2 8946  isopn2 8949  lmclimnn 9242  cdrci 10182  hmph 10241  fillsb 10270  norm-i 10629  hoeq 11323  nmopgt0 11473  elnlfn 11489  irredi 11966  addltmulALT 12018  bnj1105 12921  zmodid2 13614  absdvdsb 13673  dvdsabsb 13674  infi1 14343  fiiu 14344  cnvref 14371  domtri2 14433  cmpfun 14480  mnlmxl2 14611  dutos1 14626  seqzp2 14716  curgrpact 14735  prsubrtr 14763  nelioo5 14856  cnvhmph 14881  hmeogrp 14892  cnfilca 14927  rcfpfil 14934  limfilnei 14943  invtrgrp 14979  cntrsetlem 14999  lvsovso2 15039  supnuf 15041  supexr 15043  dualalg 15131  isfuna 15182  tarax3c 15224  vtarsuelt 15272  subtr2 15353  cbvsbcOLD 15355  ordisoOLD 15374  omsubsdomOLD 15390  compsub 15431  topbasfne 15499  limfilcf 15587  fcluscf 15612  resoprab2 15710  indexa 15753  sdc 15811  fdc 15812  caushft 15851  txmet 15925  isidlc 16163  bicomddOLD 16229  prter3 16286  pm14.122a 16386  ordintdif 16440  bitr3VD 16673  lubid 16807  latlem12 16873  opcon1b 16925  isline2 17248

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  df-an 242

Copyright terms: Public domain