Theorem bicomd 520

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 519	. 2 |- ((ps <-> ch) <-> (ch <-> ps))
3	1, 2	sylib 198	1 |- (ph -> (ch <-> ps))

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

This theorem is referenced by:  con1bid 526  bitr2d 528  bitr3d 529  bitr4d 530  syl5rbb 532  syl6rbb 536  ibir 592  pm5.54 682  baibr 685  pm5.5 731  bimsc1 749  ninba 768  sbco 1251  sbidm 1253  sbco2 1254  necon3bbid 1598  gencbvex 1835  clel3g 1889  moi2 1921  moi 1922  reu8 1933  sbhypf 1936  sbhyp 1937  r19.9rzv 2346  ifboth 2372  iununi 2612  poeq2 2839  soeq2 2850  freq2 2919  tfinds2 3161  ralxpf 3216  fconstfv 3844  isoid 3890  isoini 3895  isowe 3898  f1oweALT 3901  tfrlem5 3910  oaword 4176  oalimcl 4187  omword 4194  oeword 4210  nnaordex 4242  nnawordex 4243  pw2en 4435  carduni 4841  aleph11 4862  alephval3 4886  axrepndlem2 4928  lttri2t 5496  xrlttri2t 5538  muln0bt 5676  lemul1t 5798  lt2msq 5839  msq11 5841  nn0ind-raph 6172  rebtwnz 6180  qrecclt 6223  qsqueeze 6230  om2uzlt 6248  expne0tOLD 6532  2climnn 7055  2climnn0 7056  znnen 7462  gch-kn 7547  bastop 7602  iscld2 7630  isopn2 7633  lmclimnn 7926  norm-it 8951  nmopgt0t 9793  elnlfnt 9809  irred 10277  ompfl3 10385  rcla4devOLD 10389  infi1 10405  fiiu 10408  cmpfun 10421  cdrci 10440  hmph 10470  cnvhmph 10473  hmeogrp 10484  fillsb 10494  cnfilca 10510  rcfpfil 10517  mslb1 10545  isfuna 10664

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

Copyright terms: Public domain