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  805  con1biidc  807  con2biidc  809  pm4.63dc  816  pm4.64dc  837  pm5.55dc  855  baibr  865  baibd  868  rbaibd  869  pm4.55dc  882  anordc  900  pm5.75  906  ninba  916  xor3dc  1321  3impexpbicomi  1371  cbvexh  1682  sbequ12r  1699  sbco  1887  sbcomxyyz  1891  sbal1yz  1922  cbvab  2207  nnedc  2256  necon3bbid  2291  necon2abiidc  2315  necon2bbii  2316  gencbvex  2659  gencbval  2661  sbhypf  2662  clel3g  2742  reu8  2802  sbceq2a  2839  sbcco2  2851  sbcsng  3483  ssdifsn  3550  opabid  4056  soeq2  4115  tfisi  4373  posng  4476  xpiindim  4539  fvopab6  5352  fconstfvm  5469  cbvfo  5518  cbvexfo  5519  f1eqcocnv  5524  isoid  5543  isoini  5551  resoprab2  5692  dfoprab3  5911  cnvoprab  5949  nnacan  6216  nnmcan  6223  isotilem  6637  eqinfti  6651  inflbti  6655  infglbti  6656  djuf1olem  6681  dfmpq2  6850  div4p1lem1div2  8594  ztri3or  8718  nn0ind-raph  8788  zindd  8789  qreccl  9051  iooshf  9294  fzofzim  9519  elfzomelpfzo  9562  zmodid2  9679  q2submod  9712  modfzo0difsn  9722  frec2uzltd  9730  frec2uzled  9756  prhash2ex  10105  iiserex  10611  absdvdsb  10680  dvdsabsb  10681  modmulconst  10694  dvdsadd  10705  dvdsabseq  10714  odd2np1  10739  mod2eq0even  10744  oddnn02np1  10746  oddge22np1  10747  evennn02n  10748  evennn2n  10749  zeo5  10754  gcdass  10870  lcmdvds  10927  lcmass  10933  divgcdcoprm0  10949  divgcdcoprmex  10950  1nprm  10962  dvdsnprmd  10973  isevengcd2  11003  bj-indeq  11253
  Copyright terms: Public domain W3C validator