New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  bicomd GIF version

Theorem bicomd 192
 Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bicomd.1 (φ → (ψχ))
Assertion
Ref Expression
bicomd (φ → (χψ))

Proof of Theorem bicomd
StepHypRef Expression
1 bicomd.1 . 2 (φ → (ψχ))
2 bicom 191 . 2 ((ψχ) ↔ (χψ))
31, 2sylib 188 1 (φ → (χψ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  impbid2  195  syl5ibr  212  ibir  233  bitr2d  245  bitr3d  246  bitr4d  247  syl5rbb  249  syl6rbb  253  con1bid  320  pm5.5  326  anabs5  784  pm5.55  867  pm5.54  870  baibr  872  baibd  875  rbaibd  876  pm5.75  903  ninba  927  3impexpbicomi  1368  cad1  1398  sbequ12r  1920  sbco  2083  sbco2  2086  cbvab  2471  necon3bbid  2550  necon4bbid  2581  ralcom2  2775  gencbvex  2901  sbhypf  2904  clel3g  2976  reu8  3032  sbceq2a  3057  sbcco2  3069  r19.9rzv  3644  sbcsng  3783  opkelcokg  4261  elssetkg  4269  nnsucelrlem2  4425  opabid  4695  fconstfv  5456  isoid  5490  isoini  5497  funsi  5520  resoprab2  5582  nmembers1lem3  6270  epelcres  6328
 Copyright terms: Public domain W3C validator