Theorem biimprcd 250

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimparc  479  ax12i  1968  moanimlem  2619  euan  2622  euanv  2625  eleq1a  2832  ceqsalgALT  3467  cgsexg  3475  cgsex2g  3476  cgsex4g  3477  spcegv  3540  spc2egv  3542  reu6  3673  csbiebt  3867  reusv2lem2  5338  ralxfrALT  5354  axprlem4  5365  sotr3  5575  opelxp  5662  ssrel  5734  ssrel2  5736  ssrelrel  5747  iss  5996  ordun  6425  fprb  7144  riotaclb  7360  iunpw  7720  limom  7828  funcnvuni  7878  fiunlem  7890  soxp  8074  tfrlem8  8318  oaordex  8488  eroveu  8754  fundmen  8973  nneneq  9135  onfin2  9146  dif1ennnALT  9182  unfilem1  9210  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  21116  fvmptnn04ifb  22830  fbasfip  23847  alexsubALTlem2  24027  ovolunlem1  25478  dchrisum0flb  27491  nodmon  27632  noextendseq  27649  nocvxminlem  27764  brbtwn2  28992  axcontlem8  29058  isclwwlknx  30125  clwwlkel  30135  clwwlknwwlksnb  30144  wwlksext2clwwlk  30146  mdbr3  32387  mdbr4  32388  atssma  32468  atcvatlem  32475  ssrelf  32707  fnrelpredd  35254  nepss  35920  hfun  36380  axtco2  36676  axtcond  36680  bj-ax12ig  36935  bj-alextruim  36951  bj-substw  37042  bj-axreprepsep  37402  finxpreclem2  37726  wl-eujustlem1  37933  indexdom  38075  fdc  38086  totbndss  38118  grpomndo  38216  iss2  38685  ax12eq  39407  ax12el  39408  lsatn0  39465  lsatcmp  39469  lsatcv0  39497  lfl1dim  39587  lfl1dim2N  39588  lkrss2N  39635  lub0N  39655  glb0N  39659  ispsubcl2N  40413  cdlemefrs29bpre0  40862  dihglblem2N  41760  dihglblem3N  41761  dochsnnz  41916  pm13.14  44860  tratrb  44987  ax6e2ndeq  45010  3impexpbicomVD  45307  tratrbVD  45311  equncomVD  45318  trsbcVD  45327  sbcssgVD  45333  csbingVD  45334  onfrALTVD  45341  csbsngVD  45343  csbxpgVD  45344  csbresgVD  45345  csbrngVD  45346  csbima12gALTVD  45347  csbunigVD  45348  csbfv12gALTVD  45349  con5VD  45350  hbimpgVD  45354  hbexgVD  45356  ax6e2ndeqVD  45359  supxrleubrnmpt  45858  suprleubrnmpt  45874  infxrgelbrnmpt  45906  usgrgrtrirex  48444  isassintop  48704  zgtp1leeq  49015