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  2611  euan  2614  euanv  2617  eleq1a  2823  ceqsalgALT  3473  cgsexg  3481  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  ceqsexOLD  3486  spcegv  3552  spc2egv  3554  reu6  3686  csbiebt  3880  dfiin2g  4981  reusv2lem2  5338  ralxfrALT  5354  axprlem4  5365  sotr3  5568  opelxp  5655  ssrel  5726  ssrel2  5728  ssrelrel  5739  iss  5986  ordun  6413  fprb  7130  riotaclb  7347  iunpw  7707  limom  7815  funcnvuni  7865  fiunlem  7877  soxp  8062  tfrlem8  8306  oaordex  8476  eroveu  8739  fundmen  8956  nneneq  9120  onfin2  9130  dif1ennnALT  9166  unfilem1  9194  rankwflemb  9689  sornom  10171  isf32lem9  10255  axdc3lem2  10345  axdc4lem  10349  zorn2lem3  10392  zorn2lem7  10396  tskuni  10677  grur1a  10713  grothomex  10723  genpnnp  10899  ltaddpr  10928  reclem4pr  10944  supadd  12093  supmullem1  12095  uzin  12775  elfzmlbp  13542  isfinite4  14269  brfi1uzind  14415  swrdnd  14561  01sqrexlem6  15154  sqreulem  15267  fvprmselgcd1  16957  lubun  18421  lspsneq  21029  fvmptnn04ifb  22736  fbasfip  23753  alexsubALTlem2  23933  ovolunlem1  25396  dchrisum0flb  27419  nodmon  27560  noextendseq  27577  nocvxminlem  27688  brbtwn2  28854  axcontlem8  28920  isclwwlknx  29984  clwwlkel  29994  clwwlknwwlksnb  30003  wwlksext2clwwlk  30005  mdbr3  32245  mdbr4  32246  atssma  32326  atcvatlem  32333  ssrelf  32567  fnrelpredd  35072  nepss  35711  hfun  36172  bj-ax12ig  36630  bj-substw  36716  finxpreclem2  37384  indexdom  37734  fdc  37745  totbndss  37777  grpomndo  37875  iss2  38332  ax12eq  38940  ax12el  38941  lsatn0  38998  lsatcmp  39002  lsatcv0  39030  lfl1dim  39120  lfl1dim2N  39121  lkrss2N  39168  lub0N  39188  glb0N  39192  ispsubcl2N  39946  cdlemefrs29bpre0  40395  dihglblem2N  41293  dihglblem3N  41294  dochsnnz  41449  pm13.14  44402  tratrb  44530  ax6e2ndeq  44553  3impexpbicomVD  44850  tratrbVD  44854  equncomVD  44861  trsbcVD  44870  sbcssgVD  44876  csbingVD  44877  onfrALTVD  44884  csbsngVD  44886  csbxpgVD  44887  csbresgVD  44888  csbrngVD  44889  csbima12gALTVD  44890  csbunigVD  44891  csbfv12gALTVD  44892  con5VD  44893  hbimpgVD  44897  hbexgVD  44899  ax6e2ndeqVD  44902  supxrleubrnmpt  45405  suprleubrnmpt  45421  infxrgelbrnmpt  45453  usgrgrtrirex  47954  isassintop  48214  zgtp1leeq  48526