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

Theorem biimpcd 224
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 22 . 2  |-  ( ps 
->  ps )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibcom 220 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  biimpac  486  axc16i  2050  nelneq  2560  nelneq2  2561  nelne1  2772  nelne2  2773  nssne1  3545  nssne2  3546  psssstr  3595  difsn  4149  iununi  4400  disjiun  4427  nbrne1  4454  nbrne2  4455  mosubopt  4735  tz7.7  4894  issref  5370  tz6.12i  5876  ssimaex  5923  chfnrn  5983  fvn0ssdmfun  6007  ffnfv  6042  f1elima  6156  elovmpt3rab1  6521  limsssuc  6670  nnsuc  6702  peano5  6708  dftpos4  6976  odi  7230  fineqvlem  7736  pssnn  7740  ordunifi  7772  wdom2d  8009  r1pwss  8205  alephval3  8494  infdif  8592  cff1  8641  cofsmo  8652  axdc3lem2  8834  zorn2lem6  8884  cfpwsdom  8962  prub  9375  prnmadd  9378  1re  9598  letr  9681  dedekindle  9748  addid1  9763  xrletr  11372  0fz1  11716  elfzmlbp  11797  leisorel  12491  exprelprel  12510  brfi1uzind  12514  swrdccatfn  12689  sqrmo  13067  dvdseq  14015  isprm2  14207  nprmdvds1  14234  pltletr  15580  mgm2nsgrplem3  16017  sgrp2nmndlem3  16022  fvcosymgeq  16433  sylow2alem2  16617  islss  17560  assamulgscmlem2  17977  gsumply1subr  18254  gzrngunitlem  18461  pjdm2  18720  dmatmul  18977  decpmatmullem  19250  monmat2matmon  19303  chpscmat  19321  chfacfscmulgsum  19339  chfacfpmmulgsum  19343  isclo2  19567  fbasfip  20347  ufileu  20398  alexsubALTlem2  20526  cnextcn  20545  metustblOLD  21061  metustbl  21062  usgrarnedg1  24367  nbgraf1olem3  24421  nbgraf1olem5  24423  nb3graprlem1  24429  cusgrafilem2  24458  wlkn0  24505  fargshiftfo  24616  3v3e3cycl1  24622  4cycl4v4e  24644  4cycl4dv4e  24646  wlkiswwlk2lem3  24671  wlklniswwlkn1  24677  wlklniswwlkn2  24678  wwlknext  24702  clwwlknimp  24754  clwlkisclwwlklem2a1  24757  clwlkisclwwlklem2a  24763  clwwlkel  24771  clwwlkext2edg  24780  wwlkext2clwwlk  24781  clwwisshclwwlem  24784  hashecclwwlkn1  24812  usghashecclwwlk  24813  clwlkfclwwlk  24822  clwlkf1clwwlklem2  24825  el2wlkonot  24847  el2wlkonotot1  24852  frgrancvvdeqlemA  25015  frgrancvvdeqlemC  25017  frgraeu  25032  numclwlk2lem2f  25081  numclwlk2lem2f1o  25083  frgraogt3nreg  25098  ismgmOLD  25300  5oalem6  26555  eigorthi  26734  adjbd1o  26982  dmdbr7ati  27321  dfpo2  29160  fundmpss  29172  funbreq  29177  idinside  29710  sdclem2  30211  fdc1  30215  lptioo2  31591  lptioo1  31592  funressnfv  32167  ffnafv  32210  usgedgimp  32357  usgedgimpALT  32360  fusgraimpcl  32381  fusgraimpclALT  32383  fusgraimpclALT2  32385  mgmpropd  32417  funcestrcsetclem8  32619  funcestrcsetclem9  32620  fthestrcsetc  32622  fullestrcsetc  32623  funcsetcestrclem9  32635  fthsetcestrc  32637  fullsetcestrc  32638  rngcinv  32664  rngcinvOLD  32676  ringcinv  32712  ringcinvOLD  32736  srhmsubc  32752  srhmsubcOLD  32771  3impexpbicom  33089  sbcim2g  33177  suctrALT2VD  33504  suctrALT2  33505  3impexpVD  33524  3impexpbicomVD  33525  sbcim2gVD  33543  csbeq2gVD  33560  csbsngVD  33561  ax6e2ndeqVD  33577  2sb5ndVD  33578  bj-eldiag2  34482  lsatcvatlem  34649  atnle  34917  cvratlem  35020  ispsubcl2N  35546  trlord  36170  diaelrnN  36647  cdlemm10N  36720  dochexmidlem7  37068
  Copyright terms: Public domain W3C validator