Theorem biimprcd 252

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimparc  481  ax12i  1974  moanimlem  2624  euan  2627  euanv  2630  eleq1a  2836  ceqsalgALT  3469  cgsexg  3477  cgsex2g  3478  cgsex4g  3479  spcegv  3537  spc2egv  3539  reu6  3669  csbiebt  3862  reusv2lem2  5331  ralxfrALT  5347  axprlem4  5358  sotr3  5570  opelxp  5657  ssrel  5729  ssrel2  5731  ssrelrel  5742  iss  5994  ordun  6420  fprb  7142  riotaclb  7358  iunpw  7718  limom  7826  funcnvuni  7876  fiunlem  7888  soxp  8073  tfrlem8  8317  oaordex  8487  eroveu  8753  fundmen  8972  nneneq  9134  onfin2  9145  dif1ennnALT  9181  unfilem1  9209  elirrv  9506  rankwflemb  9712  sornom  10194  isf32lem9  10278  axdc3lem2  10368  axdc4lem  10372  zorn2lem3  10415  zorn2lem7  10419  tskuni  10701  grur1a  10737  grothomex  10747  genpnnp  10923  ltaddpr  10952  reclem4pr  10968  supadd  12119  supmullem1  12121  uzin  12819  elfzmlbp  13588  isfinite4  14319  brfi1uzind  14465  swrdnd  14612  01sqrexlem6  15204  sqreulem  15317  fvprmselgcd1  17011  lubun  18476  lspsneq  21119  fvmptnn04ifb  22838  fbasfip  23855  alexsubALTlem2  24035  ovolunlem1  25486  dchrisum0flb  27495  nodmon  27636  noextendseq  27653  nocvxminlem  27768  brbtwn2  28996  axcontlem8  29062  isclwwlknx  30128  clwwlkel  30138  clwwlknwwlksnb  30147  wwlksext2clwwlk  30149  mdbr3  32390  mdbr4  32391  atssma  32471  atcvatlem  32478  ssrelf  32711  fnrelpredd  35287  nepss  35961  hfun  36421  axtco2  36717  axtcond  36721  bj-ax12ig  36976  bj-alextruim  36992  bj-substw  37083  bj-axreprepsep  37443  finxpreclem2  37767  wl-eujustlem1  37974  indexdom  38116  fdc  38127  totbndss  38159  grpomndo  38257  iss2  38726  ax12eq  39448  ax12el  39449  lsatn0  39506  lsatcmp  39510  lsatcv0  39538  lfl1dim  39628  lfl1dim2N  39629  lkrss2N  39676  lub0N  39696  glb0N  39700  ispsubcl2N  40454  cdlemefrs29bpre0  40903  dihglblem2N  41801  dihglblem3N  41802  dochsnnz  41957  pm13.14  44868  tratrb  44995  ax6e2ndeq  45018  3impexpbicomVD  45315  tratrbVD  45319  equncomVD  45326  trsbcVD  45335  sbcssgVD  45341  csbingVD  45342  onfrALTVD  45349  csbsngVD  45351  csbxpgVD  45352  csbresgVD  45353  csbrngVD  45354  csbima12gALTVD  45355  csbunigVD  45356  csbfv12gALTVD  45357  con5VD  45358  hbimpgVD  45362  hbexgVD  45364  ax6e2ndeqVD  45367  supxrleubrnmpt  45863  suprleubrnmpt  45879  infxrgelbrnmpt  45911  usgrgrtrirex  48455  isassintop  48715  zgtp1leeq  49026