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  478  ax12i  1963  moanimlem  2607  euan  2610  euanv  2613  eleq1a  2821  ceqsalgALT  3500  cgsexg  3510  cgsex2g  3511  cgsex4g  3512  cgsex4gOLD  3513  ceqsexOLD  3515  ceqsexvOLD  3517  spcegv  3583  spc2egv  3585  reu6  3720  csbiebt  3922  dfiin2g  5033  reusv2lem2  5394  ralxfrALT  5410  sotr3  5624  opelxp  5709  ssrel  5779  ssrelOLD  5780  ssrel2  5782  ssrelrel  5793  iss  6035  ordun  6470  fprb  7201  riotaclb  7412  iunpw  7769  limom  7882  funcnvuni  7935  fiunlem  7945  soxp  8133  tfrlem8  8404  oaordex  8578  eroveu  8831  fundmen  9057  nneneq  9234  nneneqOLD  9246  onfin2  9256  dif1ennnALT  9302  unfilem1  9335  rankwflemb  9827  sornom  10309  isf32lem9  10393  axdc3lem2  10483  axdc4lem  10487  zorn2lem3  10530  zorn2lem7  10534  tskuni  10815  grur1a  10851  grothomex  10861  genpnnp  11037  ltaddpr  11066  reclem4pr  11082  supadd  12226  supmullem1  12228  uzin  12906  elfzmlbp  13658  isfinite4  14372  brfi1uzind  14510  swrdnd  14655  01sqrexlem6  15245  sqreulem  15357  fvprmselgcd1  17040  lubun  18533  lspsneq  21097  fvmptnn04ifb  22839  fbasfip  23858  alexsubALTlem2  24038  ovolunlem1  25512  dchrisum0flb  27534  nodmon  27675  noextendseq  27692  nocvxminlem  27802  brbtwn2  28834  axcontlem8  28900  isclwwlknx  29964  clwwlkel  29974  clwwlknwwlksnb  29983  wwlksext2clwwlk  29985  mdbr3  32225  mdbr4  32226  atssma  32306  atcvatlem  32313  ssrelf  32533  fnrelpredd  34937  nepss  35551  hfun  36013  bj-ax12ig  36351  bj-substw  36438  finxpreclem2  37108  indexdom  37446  fdc  37457  totbndss  37489  grpomndo  37587  iss2  38053  ax12eq  38650  ax12el  38651  lsatn0  38708  lsatcmp  38712  lsatcv0  38740  lfl1dim  38830  lfl1dim2N  38831  lkrss2N  38878  lub0N  38898  glb0N  38902  ispsubcl2N  39657  cdlemefrs29bpre0  40106  dihglblem2N  41004  dihglblem3N  41005  dochsnnz  41160  pm13.14  44118  tratrb  44247  ax6e2ndeq  44270  3impexpbicomVD  44568  tratrbVD  44572  equncomVD  44579  trsbcVD  44588  sbcssgVD  44594  csbingVD  44595  onfrALTVD  44602  csbsngVD  44604  csbxpgVD  44605  csbresgVD  44606  csbrngVD  44607  csbima12gALTVD  44608  csbunigVD  44609  csbfv12gALTVD  44610  con5VD  44611  hbimpgVD  44615  hbexgVD  44617  ax6e2ndeqVD  44620  supxrleubrnmpt  45055  suprleubrnmpt  45071  infxrgelbrnmpt  45103  isassintop  47621  zgtp1leeq  47938