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 22	. 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  483  ax12i  1975  moanimlem  2619  euan  2622  euanv  2625  eleq1a  2826  ceqsalgALT  3431  cgsexg  3440  cgsex2g  3441  cgsex4g  3442  cgsex4gOLD  3443  ceqsex  3444  ceqsexv  3445  spcegv  3502  spc2egv  3504  reu6  3628  csbiebt  3828  dfiin2g  4927  reusv2lem2  5277  ralxfrALT  5293  opelxp  5572  ssrel  5639  ssrel2  5641  ssrelrel  5651  iss  5888  ordun  6292  fprb  6987  riotaclb  7190  iunpw  7534  limom  7638  funcnvuni  7687  fiunlem  7693  soxp  7874  tfrlem8  8098  oaordex  8264  eroveu  8472  fundmen  8686  nneneq  8807  onfin2  8847  dif1enOLD  8885  unfilem1  8913  rankwflemb  9374  sornom  9856  isf32lem9  9940  axdc3lem2  10030  axdc4lem  10034  zorn2lem3  10077  zorn2lem7  10081  tskuni  10362  grur1a  10398  grothomex  10408  genpnnp  10584  ltaddpr  10613  reclem4pr  10629  supadd  11765  supmullem1  11767  uzin  12439  elfzmlbp  13188  isfinite4  13894  brfi1uzind  14029  swrdnd  14184  sqrlem6  14776  sqreulem  14888  fvprmselgcd1  16561  lubun  17975  lspsneq  20113  fvmptnn04ifb  21702  fbasfip  22719  alexsubALTlem2  22899  ovolunlem1  24348  dchrisum0flb  26345  brbtwn2  26950  axcontlem8  27016  isclwwlknx  28073  clwwlkel  28083  clwwlknwwlksnb  28092  wwlksext2clwwlk  28094  mdbr3  30332  mdbr4  30333  atssma  30413  atcvatlem  30420  ssrelf  30628  fnrelpredd  32728  nepss  33331  sotr3  33403  nodmon  33539  noextendseq  33556  nocvxminlem  33658  hfun  34166  bj-ax12ig  34503  bj-substw  34590  finxpreclem2  35247  indexdom  35578  fdc  35589  totbndss  35621  grpomndo  35719  iss2  36165  ax12eq  36641  ax12el  36642  lsatn0  36699  lsatcmp  36703  lsatcv0  36731  lfl1dim  36821  lfl1dim2N  36822  lkrss2N  36869  lub0N  36889  glb0N  36893  ispsubcl2N  37647  cdlemefrs29bpre0  38096  dihglblem2N  38994  dihglblem3N  38995  dochsnnz  39150  pm13.14  41641  tratrb  41770  ax6e2ndeq  41793  3impexpbicomVD  42091  tratrbVD  42095  equncomVD  42102  trsbcVD  42111  sbcssgVD  42117  csbingVD  42118  onfrALTVD  42125  csbsngVD  42127  csbxpgVD  42128  csbresgVD  42129  csbrngVD  42130  csbima12gALTVD  42131  csbunigVD  42132  csbfv12gALTVD  42133  con5VD  42134  hbimpgVD  42138  hbexgVD  42140  ax6e2ndeqVD  42143  supxrleubrnmpt  42560  suprleubrnmpt  42576  infxrgelbrnmpt  42610  isassintop  45020  zgtp1leeq  45478