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

Theorem biimpcd 217
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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpcd  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem biimpcd
StepHypRef Expression
1 id 21 . 2  |-  ( ps 
->  ps )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibcom 213 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  biimpac  474  3impexpbicom  1377  ax16i  2052  nfsb4tOLD  2130  ax16ALT2  2157  nelneq  2536  nelneq2  2537  nelne1  2695  nelne2  2696  nssne1  3406  nssne2  3407  psssstr  3455  difsn  3935  iununi  4178  disjiun  4205  nbrne1  4232  nbrne2  4233  mosubopt  4457  tz7.7  4610  limsssuc  4833  nnsuc  4865  peano5  4871  issref  5250  tz6.12i  5754  ssimaex  5791  chfnrn  5844  ffnfv  5897  f1elima  6012  dftpos4  6501  odi  6825  fineqvlem  7326  pssnn  7330  ordunifi  7360  wdom2d  7551  r1pwss  7713  alephval3  7996  infdif  8094  cff1  8143  cofsmo  8154  axdc3lem2  8336  zorn2lem6  8386  cfpwsdom  8464  prub  8876  prnmadd  8879  1re  9095  letr  9172  addid1  9251  xrletr  10753  0fz1  11079  leisorel  11714  brfi1uzind  11720  sqrmo  12062  dvdseq  12902  isprm2  13092  nprmdvds1  13116  pltletr  14433  sylow2alem2  15257  islss  16016  gzrngunitlem  16768  pjdm2  16943  isclo2  17157  fbasfip  17905  ufileu  17956  alexsubALTlem2  18084  cnextcn  18103  metustblOLD  18615  metustbl  18616  usgrarnedg1  21413  nbgraf1olem3  21458  nbgraf1olem5  21460  nb3graprlem1  21465  cusgrafilem2  21494  fargshiftfo  21630  3v3e3cycl1  21636  4cycl4v4e  21658  4cycl4dv4e  21660  ismgm  21913  5oalem6  23166  eigorthi  23345  adjbd1o  23593  dmdbr7ati  23932  dedekindle  25193  dfpo2  25383  fundmpss  25395  funbreq  25400  idinside  26023  wl-pm5.74lem  26232  sdclem2  26460  fdc1  26464  funressnfv  27982  ffnafv  28025  elfzmlbp  28130  ubmelfzo  28149  exprelprel  28196  swrdccatfn  28238  cshweqdif2  28304  cshweqdif2s  28305  wlkn0  28332  wlkiswwlk2lem3  28375  wlklniswwlkn1  28381  wlklniswwlkn2  28382  el2wlkonot  28401  el2wlkonotot1  28406  frgrancvvdeqlemA  28500  frgrancvvdeqlemC  28502  frgraeu  28517  sbcim2g  28697  suctrALT2VD  29022  suctrALT2  29023  3impexpVD  29042  3impexpbicomVD  29043  sbcim2gVD  29061  csbeq2gVD  29078  csbsngVD  29079  a9e2ndeqVD  29095  2sb5ndVD  29096  ax16iNEW7  29625  nfsb4twAUX7  29650  ax16ALT2OLD7  29817  nfsb4tOLD7  29819  nfsb4tw2AUXOLD7  29820  lsatcvatlem  29921  atnle  30189  cvratlem  30292  ispsubcl2N  30818  trlord  31440  diaelrnN  31917  cdlemm10N  31990  dochexmidlem7  32338
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