ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bicomd Structured version   GIF version

Theorem bicomd 129
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 128 . 2 ((ψχ) ↔ (χψ))
31, 2sylib 127 1 (φ → (χψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  impbid2  131  syl5ibr  145  ibir  166  bitr2d  178  bitr3d  179  bitr4d  180  syl5rbb  182  syl6rbb  186  pm5.5  231  anabs5  507  con2bidc  768  con1biidc  770  con2biidc  772  pm4.63dc  779  pm4.64dc  800  pm5.55dc  818  baibr  828  baibd  831  rbaibd  832  pm4.55dc  845  anordc  862  pm5.75  868  ninba  878  xor3dc  1275  3impexpbicomi  1325  cbvexh  1635  sbequ12r  1652  sbco  1839  sbcomxyyz  1843  sbal1yz  1874  cbvab  2157  nnedc  2208  necon3bbid  2239  necon2abiidc  2263  necon2bbii  2264  gencbvex  2594  gencbval  2596  sbhypf  2597  clel3g  2672  reu8  2731  sbceq2a  2768  sbcco2  2780  sbcsng  3420  opabid  3985  soeq2  4044  tfisi  4253  posng  4355  xpiindim  4416  fvopab6  5207  fconstfvm  5322  cbvfo  5368  cbvexfo  5369  f1eqcocnv  5374  isoid  5393  isoini  5400  resoprab2  5540  dfoprab3  5759  nnacan  6021  nnmcan  6028  dfmpq2  6339  ztri3or  8024  nn0ind-raph  8091  zindd  8092  qreccl  8311  iooshf  8551  fzofzim  8774  elfzomelpfzo  8817  frec2uzltd  8830  bj-indeq  9318
  Copyright terms: Public domain W3C validator