Theorem biimprcd 239

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  biimparc  503  ax12i  1866  moanim  2517  euan  2518  eleq1a  2683  ceqsalgALT  3204  cgsexg  3211  cgsex2g  3212  cgsex4g  3213  ceqsex  3214  spc2egv  3268  spc3egv  3270  reu6  3362  csbiebt  3519  dfiin2g  4489  reusv2lem2  4795  ralxfrALT  4813  opelxp  5070  ssrel  5130  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  iss  5367  ordun  5746  riotaclb  6548  iunpw  6870  limom  6972  funcnvuni  7012  fun11iun  7019  soxp  7177  tfrlem8  7367  oaordex  7525  eroveu  7729  fundmen  7916  nneneq  8028  onfin2  8037  dif1en  8078  unfilem1  8109  rankwflemb  8539  sornom  8982  isf32lem9  9066  axdc3lem2  9156  axdc4lem  9160  zorn2lem3  9203  zorn2lem7  9207  tskuni  9484  grur1a  9520  grothomex  9530  genpnnp  9706  ltaddpr  9735  reclem4pr  9751  supadd  10868  supmullem1  10870  uzin  11596  elfzmlbp  12319  isfinite4  13014  brfi1uzind  13135  brfi1uzindOLD  13141  swrdnd  13284  sqrlem6  13836  sqreulem  13947  isprm2lem  15232  fvprmselgcd1  15587  lubun  16946  lspsneq  18943  fvmptnn04ifb  20475  fbasfip  21482  alexsubALTlem2  21662  ovolunlem1  23072  dchrisum0flb  24999  brbtwn2  25585  axcontlem8  25651  usgranloopv  25907  rusgrargra  26457  frgrancvvdeqlemC  26566  mdbr3  28540  mdbr4  28541  atssma  28621  atcvatlem  28628  ssrelf  28805  nepss  30854  fprb  30916  frrlem4  31027  nodmon  31047  nodenselem4  31083  nocvxminlem  31089  nofulllem4  31104  nofulllem5  31105  hfun  31455  bj-ax12ig  31802  bj-ax12iOLD  31804  finxpreclem2  32403  indexdom  32699  fdc  32711  totbndss  32746  grpomndo  32844  ax12eq  33244  ax12el  33245  lsatn0  33304  lsatcmp  33308  lsatcv0  33336  lfl1dim  33426  lfl1dim2N  33427  lkrss2N  33474  lub0N  33494  glb0N  33498  ispsubcl2N  34251  cdlemefrs29bpre0  34702  dihglblem2N  35601  dihglblem3N  35602  dochsnnz  35757  pm13.14  37632  tratrb  37767  ax6e2ndeq  37796  3impexpbicomVD  38114  tratrbVD  38119  equncomVD  38126  trsbcVD  38135  sbcssgVD  38141  csbingVD  38142  onfrALTVD  38149  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  con5VD  38158  hbimpgVD  38162  hbexgVD  38164  ax6e2ndeqVD  38167  frgrncvvdeqlemC  41478  isassintop  41636  zgtp1leeq  42105