Theorem biimpcd 227

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

Step	Hyp	Ref	Expression
1		id 23	. 2 |- ( ps -> ps )
2		biimpcd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5ibcom 223	1 |- ( ps -> ( ph -> ch ) )

Syntax hints:   -> wi 4   <-> wb 187

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 188

This theorem is referenced by:  biimpac  488  axc16i  2117  nelneq  2537  nelneq2  2538  nelne1  2751  nelne2  2752  nssne1  3517  nssne2  3518  psssstr  3568  difsn  4128  iununi  4381  disjiun  4408  nbrne1  4434  nbrne2  4435  mosubopt  4710  issref  5224  tz7.7  5459  tz6.12i  5892  ssimaex  5937  chfnrn  5999  fvn0ssdmfun  6019  ffnfv  6055  f1elima  6170  elovmpt3rab1  6532  limsssuc  6682  nnsuc  6714  peano5  6721  dftpos4  6991  odi  7279  fineqvlem  7783  pssnn  7787  ordunifi  7818  wdom2d  8086  r1pwss  8245  alephval3  8530  infdif  8628  cff1  8677  cofsmo  8688  axdc3lem2  8870  zorn2lem6  8920  cfpwsdom  8998  prub  9408  prnmadd  9411  1re  9631  letr  9716  dedekindle  9787  addid1  9802  negf1o  10038  negfi  10543  xrletr  11444  0fz1  11806  elfzmlbp  11889  leisorel  12607  exprelprel  12626  brfi1uzind  12630  swrdnd  12762  swrdccatfn  12812  sqrmo  13283  dvdseq  14319  isprm2  14592  nprmdvds1  14610  catsubcat  15688  funcestrcsetclem8  15976  funcestrcsetclem9  15977  fthestrcsetc  15979  fullestrcsetc  15980  funcsetcestrclem9  15992  fthsetcestrc  15994  fullsetcestrc  15995  pltletr  16161  mgm2nsgrplem3  16598  sgrp2nmndlem3  16603  fvcosymgeq  17014  sylow2alem2  17198  islss  18086  assamulgscmlem2  18501  gsumply1subr  18755  gzrngunitlem  18960  pjdm2  19198  dmatmul  19446  decpmatmullem  19719  monmat2matmon  19772  chpscmat  19790  chfacfscmulgsum  19808  chfacfpmmulgsum  19812  isclo2  20028  fbasfip  20807  ufileu  20858  alexsubALTlem2  20987  cnextcn  21006  metustbl  21505  usgrarnedg1  24959  nbgraf1olem3  25013  nbgraf1olem5  25015  nb3graprlem1  25021  cusgrafilem2  25050  wlkn0  25097  fargshiftfo  25208  3v3e3cycl1  25214  4cycl4v4e  25236  4cycl4dv4e  25238  wlkiswwlk2lem3  25263  wlklniswwlkn1  25269  wlklniswwlkn2  25270  wwlknext  25294  clwwlknimp  25346  clwlkisclwwlklem2a1  25349  clwlkisclwwlklem2a  25355  clwwlkel  25363  clwwlkext2edg  25372  wwlkext2clwwlk  25373  clwwisshclwwlem  25376  hashecclwwlkn1  25404  usghashecclwwlk  25405  clwlkfclwwlk  25414  clwlkf1clwwlklem2  25417  el2wlkonot  25439  el2wlkonotot1  25444  frgrancvvdeqlemA  25607  frgrancvvdeqlemC  25609  frgraeu  25624  numclwlk2lem2f  25673  numclwlk2lem2f1o  25675  frgraogt3nreg  25690  ismgmOLD  25890  5oalem6  27144  eigorthi  27322  adjbd1o  27570  dmdbr7ati  27909  dfpo2  30179  fundmpss  30191  funbreq  30195  idinside  30633  bj-eldiag2  31389  poimirlem32  31676  sdclem2  31775  fdc1  31779  lsatcvatlem  32324  atnle  32592  cvratlem  32695  ispsubcl2N  33221  trlord  33845  diaelrnN  34322  cdlemm10N  34395  dochexmidlem7  34743  3impexpbicom  36475  sbcim2g  36540  suctrALT2VD  36876  suctrALT2  36877  3impexpVD  36896  3impexpbicomVD  36897  sbcim2gVD  36916  csbeq2gVD  36933  csbsngVD  36934  ax6e2ndeqVD  36950  2sb5ndVD  36951  lptioo2  37287  lptioo1  37288  funressnfv  38033  ffnafv  38076  iccpartiltu  38139  iccpartigtl  38140  icceuelpartlem  38152  oddprmuzge3  38244  bgoldbtbndlem2  38304  usgedgimp  38486  usgedgimpALT  38489  fusgraimpcl  38510  fusgraimpclALT  38512  fusgraimpclALT2  38514  mgmpropd  38546  rngcinv  38754  rngcinvALTV  38766  ringcinv  38805  ringcinvALTV  38829  srhmsubc  38849  srhmsubcALTV  38868  nnolog2flm1  39175