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

Theorem bicomd 140
 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 139 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 121 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  impbid2  142  syl5ibr  155  ibir  176  bitr2d  188  bitr3d  189  bitr4d  190  syl5rbb  192  syl6rbb  196  pm5.5  241  anabs5  563  con2bidc  861  con1biidc  863  con2biidc  865  pm4.63dc  872  pm4.64dc  886  pm5.55dc  899  baibr  906  baibd  909  rbaibd  910  pm4.55dc  923  anordc  941  pm5.75  947  ninba  957  xor3dc  1366  3impexpbicomi  1416  cbvexh  1729  sbequ12r  1746  sbco  1942  sbcomxyyz  1946  sbal1yz  1977  cbvab  2264  nnedc  2314  necon3bbid  2349  necon2abiidc  2373  necon2bbiidc  2374  sbralie  2674  gencbvex  2736  gencbval  2738  sbhypf  2739  clel3g  2824  reu8  2885  sbceq2a  2924  sbcco2  2936  sbcsng  3591  ssdifsn  3660  opabid  4188  soeq2  4247  tfisi  4510  posng  4620  xpiindim  4685  fvopab6  5526  fconstfvm  5647  cbvfo  5695  cbvexfo  5696  f1eqcocnv  5701  isoid  5720  isoini  5728  resoprab2  5877  dfoprab3  6098  cnvoprab  6140  nnacan  6417  nnmcan  6424  isotilem  6903  eqinfti  6917  inflbti  6921  infglbti  6922  djuf1olem  6948  dfmpq2  7207  axsuploc  7881  div4p1lem1div2  9017  ztri3or  9141  nn0ind-raph  9212  zindd  9213  qreccl  9481  elpq  9487  iooshf  9785  fzofzim  10016  elfzomelpfzo  10059  zmodid2  10176  q2submod  10209  modfzo0difsn  10219  frec2uzltd  10227  frec2uzled  10253  prhash2ex  10607  iserex  11160  prodrbdc  11395  reef11  11462  absdvdsb  11567  dvdsabsb  11568  modmulconst  11581  dvdsadd  11592  dvdsabseq  11601  odd2np1  11626  mod2eq0even  11631  oddnn02np1  11633  oddge22np1  11634  evennn02n  11635  evennn2n  11636  zeo5  11641  gcdass  11759  lcmdvds  11816  lcmass  11822  divgcdcoprm0  11838  divgcdcoprmex  11839  1nprm  11851  dvdsnprmd  11862  isevengcd2  11892  bj-indeq  13318
 Copyright terms: Public domain W3C validator