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

Theorem bicomd 133
 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 132 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 131 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  impbid2  135  syl5ibr  149  ibir  170  bitr2d  182  bitr3d  183  bitr4d  184  syl5rbb  186  syl6rbb  190  pm5.5  235  anabs5  515  con2bidc  780  con1biidc  782  con2biidc  784  pm4.63dc  791  pm4.64dc  812  pm5.55dc  830  baibr  840  baibd  843  rbaibd  844  pm4.55dc  857  anordc  874  pm5.75  880  ninba  890  xor3dc  1294  3impexpbicomi  1344  cbvexh  1654  sbequ12r  1671  sbco  1858  sbcomxyyz  1862  sbal1yz  1893  cbvab  2176  nnedc  2225  necon3bbid  2260  necon2abiidc  2284  necon2bbii  2285  gencbvex  2617  gencbval  2619  sbhypf  2620  clel3g  2700  reu8  2759  sbceq2a  2796  sbcco2  2808  sbcsng  3456  opabid  4021  soeq2  4080  tfisi  4337  posng  4439  xpiindim  4500  fvopab6  5291  fconstfvm  5406  cbvfo  5452  cbvexfo  5453  f1eqcocnv  5458  isoid  5477  isoini  5484  resoprab2  5625  dfoprab3  5844  cnvoprab  5882  nnacan  6115  nnmcan  6122  isotilem  6409  dfmpq2  6510  div4p1lem1div2  8234  ztri3or  8344  nn0ind-raph  8413  zindd  8414  qreccl  8673  iooshf  8921  fzofzim  9145  elfzomelpfzo  9188  zmodid2  9301  q2submod  9334  modfzo0difsn  9344  frec2uzltd  9352  iiserex  10089  absdvdsb  10125  dvdsabsb  10126  modmulconst  10138  dvdsadd  10149  dvdsabseq  10158  odd2np1  10183  mod2eq0even  10188  oddnn02np1  10191  oddge22np1  10192  evennn02n  10193  evennn2n  10194  zeo5  10199  bj-indeq  10426
 Copyright terms: Public domain W3C validator