Theorem biimprcd 253

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 23	. 2 ⊢ (𝜒 → 𝜒)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibrcom 250	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  biimparc  484  ax12i  1993  moanimlem  2652  euan  2655  euanv  2658  eleq1a  2864  ceqsalgALT  3497  cgsexg  3505  cgsex2g  3506  cgsex4g  3507  spcegv  3563  spc2egv  3565  reu6  3696  csbiebt  3888  reusv2lem2  5371  ralxfrALT  5387  axprlem4  5398  sotr3  5611  opelxp  5698  ssrel  5770  ssrel2  5772  ssrelrel  5783  iss  6038  ordun  6468  fprb  7193  riotaclb  7409  iunpw  7770  limom  7878  funcnvuni  7929  fiunlem  7939  soxp  8125  tfrlem8  8371  oaordex  8543  eroveu  8810  fundmen  9028  nneneq  9190  onfin2  9201  dif1ennnALT  9237  unfilem1  9265  elirrv  9559  rankwflemb  9765  sornom  10261  isf32lem9  10345  axdc3lem2  10435  axdc4lem  10439  zorn2lem3  10482  zorn2lem7  10486  tskuni  10768  grur1a  10804  grothomex  10814  genpnnp  10990  ltaddpr  11019  reclem4pr  11035  supadd  12183  supmullem1  12185  uzin  12898  elfzmlbp  13667  isfinite4  14398  brfi1uzind  14545  swrdnd  14692  01sqrexlem6  15298  sqreulem  15411  fvprmselgcd1  17105  lubun  18571  lspsneq  21224  fvmptnn04ifb  22977  fbasfip  23994  alexsubALTlem2  24174  ovolunlem1  25625  dchrisum0flb  27640  nodmon  27780  noextendseq  27797  nocvxminlem  27913  brbtwn2  29196  axcontlem8  29262  isclwwlknx  30328  clwwlkel  30338  clwwlknwwlksnb  30347  wwlksext2clwwlk  30349  mdbr3  32590  mdbr4  32591  atssma  32671  atcvatlem  32678  ssrelf  32901  fnrelpredd  35425  nepss  36143  hfun  36603  nmulprop  36615  axtco2  36908  axtcond  36912  bj-ax12ig  37166  bj-alextruim  37182  bj-substw  37273  bj-axreprepsep  37635  finxpreclem2  37959  wl-eujustlem1  38166  indexdom  38308  fdc  38319  totbndss  38351  grpomndo  38449  iss2  38918  ax12eq  39640  ax12el  39641  lsatn0  39698  lsatcmp  39702  lsatcv0  39730  lfl1dim  39820  lfl1dim2N  39821  lkrss2N  39868  lub0N  39888  glb0N  39892  ispsubcl2N  40646  cdlemefrs29bpre0  41095  dihglblem2N  41993  dihglblem3N  41994  dochsnnz  42149  pm13.14  45046  tratrb  45172  ax6e2ndeq  45195  3impexpbicomVD  45492  tratrbVD  45496  equncomVD  45503  trsbcVD  45512  sbcssgVD  45518  csbingVD  45519  onfrALTVD  45526  csbsngVD  45528  csbxpgVD  45529  csbresgVD  45530  csbrngVD  45531  csbima12gALTVD  45532  csbunigVD  45533  csbfv12gALTVD  45534  con5VD  45535  hbimpgVD  45539  hbexgVD  45541  ax6e2ndeqVD  45544  supxrleubrnmpt  46047  suprleubrnmpt  46063  infxrgelbrnmpt  46095  usgrgrtrirex  48639  isassintop  48899  zgtp1leeq  49221