Theorem biimprcd 249

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 246	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimparc  480  ax12i  1970  moanimlem  2620  euan  2623  euanv  2626  eleq1a  2834  ceqsalgALT  3465  cgsexg  3474  cgsex2g  3475  cgsex4g  3476  cgsex4gOLD  3477  ceqsex  3478  ceqsexv  3479  spcegv  3536  spc2egv  3538  reu6  3661  csbiebt  3862  dfiin2g  4962  reusv2lem2  5322  ralxfrALT  5338  opelxp  5625  ssrel  5693  ssrelOLD  5694  ssrel2  5696  ssrelrel  5706  iss  5943  ordun  6367  fprb  7069  riotaclb  7274  iunpw  7621  limom  7728  funcnvuni  7778  fiunlem  7784  soxp  7970  tfrlem8  8215  oaordex  8389  eroveu  8601  fundmen  8821  nneneq  8992  nneneqOLD  9004  onfin2  9014  dif1enALT  9050  unfilem1  9078  rankwflemb  9551  sornom  10033  isf32lem9  10117  axdc3lem2  10207  axdc4lem  10211  zorn2lem3  10254  zorn2lem7  10258  tskuni  10539  grur1a  10575  grothomex  10585  genpnnp  10761  ltaddpr  10790  reclem4pr  10806  supadd  11943  supmullem1  11945  uzin  12618  elfzmlbp  13367  isfinite4  14077  brfi1uzind  14212  swrdnd  14367  sqrlem6  14959  sqreulem  15071  fvprmselgcd1  16746  lubun  18233  lspsneq  20384  fvmptnn04ifb  22000  fbasfip  23019  alexsubALTlem2  23199  ovolunlem1  24661  dchrisum0flb  26658  brbtwn2  27273  axcontlem8  27339  isclwwlknx  28400  clwwlkel  28410  clwwlknwwlksnb  28419  wwlksext2clwwlk  28421  mdbr3  30659  mdbr4  30660  atssma  30740  atcvatlem  30747  ssrelf  30955  fnrelpredd  33061  nepss  33662  sotr3  33733  nodmon  33853  noextendseq  33870  nocvxminlem  33972  hfun  34480  bj-ax12ig  34817  bj-substw  34904  finxpreclem2  35561  indexdom  35892  fdc  35903  totbndss  35935  grpomndo  36033  iss2  36479  ax12eq  36955  ax12el  36956  lsatn0  37013  lsatcmp  37017  lsatcv0  37045  lfl1dim  37135  lfl1dim2N  37136  lkrss2N  37183  lub0N  37203  glb0N  37207  ispsubcl2N  37961  cdlemefrs29bpre0  38410  dihglblem2N  39308  dihglblem3N  39309  dochsnnz  39464  pm13.14  42027  tratrb  42156  ax6e2ndeq  42179  3impexpbicomVD  42477  tratrbVD  42481  equncomVD  42488  trsbcVD  42497  sbcssgVD  42503  csbingVD  42504  onfrALTVD  42511  csbsngVD  42513  csbxpgVD  42514  csbresgVD  42515  csbrngVD  42516  csbima12gALTVD  42517  csbunigVD  42518  csbfv12gALTVD  42519  con5VD  42520  hbimpgVD  42524  hbexgVD  42526  ax6e2ndeqVD  42529  supxrleubrnmpt  42946  suprleubrnmpt  42962  infxrgelbrnmpt  42994  isassintop  45404  zgtp1leeq  45862