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

Theorem bicomd 139
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 138 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 120 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  impbid2  141  syl5ibr  154  ibir  175  bitr2d  187  bitr3d  188  bitr4d  189  syl5rbb  191  syl6rbb  195  pm5.5  240  anabs5  538  con2bidc  803  con1biidc  805  con2biidc  807  pm4.63dc  814  pm4.64dc  835  pm5.55dc  853  baibr  863  baibd  866  rbaibd  867  pm4.55dc  880  anordc  898  pm5.75  904  ninba  914  xor3dc  1319  3impexpbicomi  1369  cbvexh  1680  sbequ12r  1697  sbco  1885  sbcomxyyz  1889  sbal1yz  1920  cbvab  2205  nnedc  2254  necon3bbid  2289  necon2abiidc  2313  necon2bbii  2314  gencbvex  2656  gencbval  2658  sbhypf  2659  clel3g  2739  reu8  2799  sbceq2a  2836  sbcco2  2848  sbcsng  3475  ssdifsn  3542  opabid  4048  soeq2  4107  tfisi  4365  posng  4468  xpiindim  4531  fvopab6  5341  fconstfvm  5455  cbvfo  5504  cbvexfo  5505  f1eqcocnv  5510  isoid  5529  isoini  5536  resoprab2  5677  dfoprab3  5896  cnvoprab  5934  nnacan  6201  nnmcan  6208  isotilem  6608  eqinfti  6622  inflbti  6626  infglbti  6627  djuf1olem  6652  dfmpq2  6817  div4p1lem1div2  8561  ztri3or  8689  nn0ind-raph  8759  zindd  8760  qreccl  9022  iooshf  9265  fzofzim  9488  elfzomelpfzo  9531  zmodid2  9648  q2submod  9681  modfzo0difsn  9691  frec2uzltd  9699  frec2uzled  9725  prhash2ex  10052  iiserex  10551  absdvdsb  10594  dvdsabsb  10595  modmulconst  10608  dvdsadd  10619  dvdsabseq  10628  odd2np1  10653  mod2eq0even  10658  oddnn02np1  10660  oddge22np1  10661  evennn02n  10662  evennn2n  10663  zeo5  10668  gcdass  10784  lcmdvds  10841  lcmass  10847  divgcdcoprm0  10863  divgcdcoprmex  10864  1nprm  10876  dvdsnprmd  10887  isevengcd2  10917  bj-indeq  11167
  Copyright terms: Public domain W3C validator