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

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

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  2037  nelneq  2584  nelneq2  2585  nelne1  2796  nelne2  2797  nssne1  3560  nssne2  3561  psssstr  3610  difsn  4161  iununi  4410  disjiun  4437  nbrne1  4464  nbrne2  4465  mosubopt  4745  tz7.7  4904  issref  5380  tz6.12i  5886  ssimaex  5932  chfnrn  5992  ffnfv  6047  f1elima  6159  elovmpt3rab1  6520  limsssuc  6669  nnsuc  6701  peano5  6707  dftpos4  6974  odi  7228  fineqvlem  7734  pssnn  7738  ordunifi  7770  wdom2d  8006  r1pwss  8202  alephval3  8491  infdif  8589  cff1  8638  cofsmo  8649  axdc3lem2  8831  zorn2lem6  8881  cfpwsdom  8959  prub  9372  prnmadd  9375  1re  9595  letr  9678  dedekindle  9744  addid1  9759  xrletr  11361  0fz1  11705  elfzmlbp  11783  leisorel  12475  exprelprel  12494  brfi1uzind  12498  swrdccatfn  12670  sqrmo  13048  dvdseq  13892  isprm2  14084  nprmdvds1  14111  pltletr  15458  fvcosymgeq  16259  sylow2alem2  16444  islss  17381  assamulgscmlem2  17797  gsumply1subr  18074  gzrngunitlem  18278  pjdm2  18537  dmatmul  18794  decpmatmullem  19067  monmat2matmon  19120  chpscmat  19138  chfacfscmulgsum  19156  chfacfpmmulgsum  19160  isclo2  19383  fbasfip  20132  ufileu  20183  alexsubALTlem2  20311  cnextcn  20330  metustblOLD  20846  metustbl  20847  usgrarnedg1  24093  nbgraf1olem3  24147  nbgraf1olem5  24149  nb3graprlem1  24155  cusgrafilem2  24184  wlkn0  24231  fargshiftfo  24342  3v3e3cycl1  24348  4cycl4v4e  24370  4cycl4dv4e  24372  wlkiswwlk2lem3  24397  wlklniswwlkn1  24403  wlklniswwlkn2  24404  wwlknext  24428  clwwlknimp  24480  clwlkisclwwlklem2a1  24483  clwlkisclwwlklem2a  24489  clwwlkel  24497  clwwlkext2edg  24506  wwlkext2clwwlk  24507  clwwisshclwwlem  24510  hashecclwwlkn1  24538  usghashecclwwlk  24539  clwlkfclwwlk  24548  clwlkf1clwwlklem2  24551  el2wlkonot  24573  el2wlkonotot1  24578  frgrancvvdeqlemA  24742  frgrancvvdeqlemC  24744  frgraeu  24759  numclwlk2lem2f  24808  numclwlk2lem2f1o  24810  frgraogt3nreg  24825  ismgm  25026  5oalem6  26281  eigorthi  26460  adjbd1o  26708  dmdbr7ati  27047  dfpo2  28789  fundmpss  28801  funbreq  28806  idinside  29339  sdclem2  29866  fdc1  29870  funressnfv  31708  ffnafv  31751  usgedgimp  31898  usgedgimpALT  31901  fusgraimpcl  31922  fusgraimpclALT  31924  fusgraimpclALT2  31926  3impexpbicom  32318  sbcim2g  32407  suctrALT2VD  32734  suctrALT2  32735  3impexpVD  32754  3impexpbicomVD  32755  sbcim2gVD  32773  csbeq2gVD  32790  csbsngVD  32791  ax6e2ndeqVD  32807  2sb5ndVD  32808  lsatcvatlem  33864  atnle  34132  cvratlem  34235  ispsubcl2N  34761  trlord  35383  diaelrnN  35860  cdlemm10N  35933  dochexmidlem7  36281