MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpcd Unicode version

Theorem biimpcd 218
Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimpcd.1
Assertion
Ref Expression
biimpcd

Proof of Theorem biimpcd
StepHypRef Expression
1 id 21 . 2
2 biimpcd.1 . 2
31, 2syl5ibcom 214 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178
This theorem is referenced by:  biimpac  476  3impexpbicom  1403  axc16i  2003  axc16ALT2  2095  nelneq  2520  nelneq2  2521  nelne1  2680  nelne2  2681  nssne1  3389  nssne2  3390  psssstr  3439  difsn  3983  iununi  4230  disjiun  4257  nbrne1  4284  nbrne2  4285  mosubopt  4561  tz7.7  4716  issref  5183  tz6.12i  5680  ssimaex  5726  chfnrn  5784  ffnfv  5838  f1elima  5944  limsssuc  6431  nnsuc  6463  peano5  6469  dftpos4  6726  odi  6979  fineqvlem  7486  pssnn  7490  ordunifi  7521  wdom2d  7742  r1pwss  7938  alephval3  8227  infdif  8325  cff1  8374  cofsmo  8385  axdc3lem2  8567  zorn2lem6  8617  cfpwsdom  8695  prub  9109  prnmadd  9112  1re  9331  letr  9414  dedekindle  9480  addid1  9495  xrletr  11077  0fz1  11413  elfzmlbp  11435  leisorel  12154  brfi1uzind  12160  swrdccatfn  12314  sqrmo  12682  dvdseq  13520  isprm2  13711  nprmdvds1  13737  pltletr  15081  fvcosymgeq  15871  sylow2alem2  16054  islss  16825  gzrngunitlem  17587  pjdm2  17844  isclo2  18396  fbasfip  19145  ufileu  19196  alexsubALTlem2  19324  cnextcn  19343  metustblOLD  19855  metustbl  19856  usgrarnedg1  22986  nbgraf1olem3  23031  nbgraf1olem5  23033  nb3graprlem1  23038  cusgrafilem2  23067  fargshiftfo  23203  3v3e3cycl1  23209  4cycl4v4e  23231  4cycl4dv4e  23233  ismgm  23486  5oalem6  24741  eigorthi  24920  adjbd1o  25168  dmdbr7ati  25507  dfpo2  27267  fundmpss  27279  funbreq  27284  idinside  27817  sdclem2  28309  fdc1  28313  funressnfv  29708  ffnafv  29751  elovmpt3rab1  29837  exprelprel  29903  wlkn0  29953  wlkiswwlk2lem3  30001  wlklniswwlkn1  30007  wlklniswwlkn2  30008  wwlknext  30030  el2wlkonot  30062  el2wlkonotot1  30067  clwwlknimp  30113  clwlkisclwwlklem2a1  30115  clwlkisclwwlklem2a  30121  clwwlkel  30129  clwwlkext2edg  30138  wwlkext2clwwlk  30139  clwwisshclwwlem  30144  hashecclwwlkn1  30182  usghashecclwwlk  30183  clwlkfclwwlk  30191  clwlkf1clwwlklem2  30194  frgrancvvdeqlemA  30304  frgrancvvdeqlemC  30306  frgraeu  30321  numclwlk2lem2f  30370  numclwlk2lem2f1o  30372  frgraogt3nreg  30387  sbcim2g  30822  suctrALT2VD  31150  suctrALT2  31151  3impexpVD  31170  3impexpbicomVD  31171  sbcim2gVD  31189  csbeq2gVD  31206  csbsngVD  31207  ax6e2ndeqVD  31223  2sb5ndVD  31224  lsatcvatlem  32131  atnle  32399  cvratlem  32502  ispsubcl2N  33028  trlord  33650  diaelrnN  34127  cdlemm10N  34200  dochexmidlem7  34548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator