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  483  3impexpbicom  1416  axc16i  2013  axc16ALT2  2106  nelneq  2533  nelneq2  2534  nelne1  2693  nelne2  2694  nssne1  3402  nssne2  3403  psssstr  3452  difsn  3998  iununi  4245  disjiun  4272  nbrne1  4299  nbrne2  4300  mosubopt  4579  tz7.7  4734  issref  5201  tz6.12i  5700  ssimaex  5746  chfnrn  5804  ffnfv  5858  f1elima  5965  limsssuc  6452  nnsuc  6484  peano5  6490  dftpos4  6755  odi  7008  fineqvlem  7517  pssnn  7521  ordunifi  7552  wdom2d  7785  r1pwss  7981  alephval3  8270  infdif  8368  cff1  8417  cofsmo  8428  axdc3lem2  8610  zorn2lem6  8660  cfpwsdom  8738  prub  9153  prnmadd  9156  1re  9375  letr  9458  dedekindle  9524  addid1  9539  xrletr  11122  0fz1  11458  elfzmlbp  11480  leisorel  12199  brfi1uzind  12205  swrdccatfn  12359  sqrmo  12727  dvdseq  13565  isprm2  13756  nprmdvds1  13782  pltletr  15126  fvcosymgeq  15916  sylow2alem2  16099  islss  16940  gzrngunitlem  17723  pjdm2  17980  isclo2  18536  fbasfip  19285  ufileu  19336  alexsubALTlem2  19464  cnextcn  19483  metustblOLD  19999  metustbl  20000  usgrarnedg1  23132  nbgraf1olem3  23177  nbgraf1olem5  23179  nb3graprlem1  23184  cusgrafilem2  23213  fargshiftfo  23349  3v3e3cycl1  23355  4cycl4v4e  23377  4cycl4dv4e  23379  ismgm  23632  5oalem6  24887  eigorthi  25066  adjbd1o  25314  dmdbr7ati  25653  dfpo2  27414  fundmpss  27426  funbreq  27431  idinside  27964  sdclem2  28484  fdc1  28488  funressnfv  29882  ffnafv  29925  elovmpt3rab1  30011  exprelprel  30077  wlkn0  30127  wlkiswwlk2lem3  30175  wlklniswwlkn1  30181  wlklniswwlkn2  30182  wwlknext  30204  el2wlkonot  30236  el2wlkonotot1  30241  clwwlknimp  30287  clwlkisclwwlklem2a1  30289  clwlkisclwwlklem2a  30295  clwwlkel  30303  clwwlkext2edg  30312  wwlkext2clwwlk  30313  clwwisshclwwlem  30318  hashecclwwlkn1  30356  usghashecclwwlk  30357  clwlkfclwwlk  30365  clwlkf1clwwlklem2  30368  frgrancvvdeqlemA  30478  frgrancvvdeqlemC  30480  frgraeu  30495  numclwlk2lem2f  30544  numclwlk2lem2f1o  30546  frgraogt3nreg  30561  dmatmul  30667  sbcim2g  30986  suctrALT2VD  31314  suctrALT2  31315  3impexpVD  31334  3impexpbicomVD  31335  sbcim2gVD  31353  csbeq2gVD  31370  csbsngVD  31371  ax6e2ndeqVD  31387  2sb5ndVD  31388  lsatcvatlem  32307  atnle  32575  cvratlem  32678  ispsubcl2N  33204  trlord  33826  diaelrnN  34303  cdlemm10N  34376  dochexmidlem7  34724