Theorem bicomd 399

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

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  bicon1d 405  bitr2d 407  bitr3d 408  bitr4d 409  syl5rbb 411  syl6rbb 415  ibir 450  baibr 507  bimsc1 557  ninba 575  sbco 910  sbidm 912  sbco2 913  gencbvex 1372  vsbcint 1438  sbc19.21g 1470  r19.9rzv 1768  r19.36zv 1772  iununi 2037  poeq2 2131  soeq2 2142  freq2 2175  tfinds2 2405  fconstfv 2903  isoid 2933  isoini 2938  isowe 2941  f1oweOLD 2944  tfrlem5 2953  oacan 3150  oaword 3151  oalimcl 3162  nnaordex 3191  nnawordex 3192  pw2en 3348  carduni 3664  aleph11 3684  axrepndlem2 3739  lttri2t 4280  ltaddsubt 4357  lemul2 4396  lt2sq 4414  sq11 4416  nn0ind 4612  rebtwnz 4620  qrecclt 4646  om2uzlt 4654  znnen 4930  gch-kn 4957  ssmd2 5735  atnssm0 5765

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

metamath.org