Theorem biimprcd 250

Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypothesis

Ref	Expression
biimpcd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimprcd	⊢ (𝜒 → (𝜑 → 𝜓))

Proof of Theorem biimprcd

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜒 → 𝜒)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibrcom 247	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimparc  479  ax12i  1966  moanimlem  2612  euan  2615  euanv  2618  eleq1a  2824  ceqsalgALT  3487  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  cgsex4gOLD  3498  ceqsexOLD  3500  spcegv  3566  spc2egv  3568  reu6  3699  csbiebt  3893  dfiin2g  4998  reusv2lem2  5356  ralxfrALT  5372  axprlem4  5383  sotr3  5589  opelxp  5676  ssrel  5747  ssrelOLD  5748  ssrel2  5750  ssrelrel  5761  iss  6008  ordun  6440  fprb  7170  riotaclb  7387  iunpw  7749  limom  7860  funcnvuni  7910  fiunlem  7922  soxp  8110  tfrlem8  8354  oaordex  8524  eroveu  8787  fundmen  9004  nneneq  9175  onfin2  9185  dif1ennnALT  9228  unfilem1  9260  rankwflemb  9752  sornom  10236  isf32lem9  10320  axdc3lem2  10410  axdc4lem  10414  zorn2lem3  10457  zorn2lem7  10461  tskuni  10742  grur1a  10778  grothomex  10788  genpnnp  10964  ltaddpr  10993  reclem4pr  11009  supadd  12157  supmullem1  12159  uzin  12839  elfzmlbp  13606  isfinite4  14333  brfi1uzind  14479  swrdnd  14625  01sqrexlem6  15219  sqreulem  15332  fvprmselgcd1  17022  lubun  18480  lspsneq  21038  fvmptnn04ifb  22744  fbasfip  23761  alexsubALTlem2  23941  ovolunlem1  25404  dchrisum0flb  27427  nodmon  27568  noextendseq  27585  nocvxminlem  27695  brbtwn2  28838  axcontlem8  28904  isclwwlknx  29971  clwwlkel  29981  clwwlknwwlksnb  29990  wwlksext2clwwlk  29992  mdbr3  32232  mdbr4  32233  atssma  32313  atcvatlem  32320  ssrelf  32549  fnrelpredd  35085  nepss  35700  hfun  36161  bj-ax12ig  36619  bj-substw  36705  finxpreclem2  37373  indexdom  37723  fdc  37734  totbndss  37766  grpomndo  37864  iss2  38321  ax12eq  38929  ax12el  38930  lsatn0  38987  lsatcmp  38991  lsatcv0  39019  lfl1dim  39109  lfl1dim2N  39110  lkrss2N  39157  lub0N  39177  glb0N  39181  ispsubcl2N  39936  cdlemefrs29bpre0  40385  dihglblem2N  41283  dihglblem3N  41284  dochsnnz  41439  pm13.14  44391  tratrb  44519  ax6e2ndeq  44542  3impexpbicomVD  44839  tratrbVD  44843  equncomVD  44850  trsbcVD  44859  sbcssgVD  44865  csbingVD  44866  onfrALTVD  44873  csbsngVD  44875  csbxpgVD  44876  csbresgVD  44877  csbrngVD  44878  csbima12gALTVD  44879  csbunigVD  44880  csbfv12gALTVD  44881  con5VD  44882  hbimpgVD  44886  hbexgVD  44888  ax6e2ndeqVD  44891  supxrleubrnmpt  45395  suprleubrnmpt  45411  infxrgelbrnmpt  45443  usgrgrtrirex  47939  isassintop  48188  zgtp1leeq  48500