Theorem biimprcd 249

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimparc  479  ax12i  1971  moanimlem  2620  euan  2623  euanv  2626  eleq1a  2834  ceqsalgALT  3455  cgsexg  3464  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  ceqsex  3468  ceqsexv  3469  spcegv  3526  spc2egv  3528  reu6  3656  csbiebt  3858  dfiin2g  4958  reusv2lem2  5317  ralxfrALT  5333  opelxp  5616  ssrel  5683  ssrel2  5685  ssrelrel  5695  iss  5932  ordun  6352  fprb  7051  riotaclb  7254  iunpw  7599  limom  7703  funcnvuni  7752  fiunlem  7758  soxp  7941  tfrlem8  8186  oaordex  8351  eroveu  8559  fundmen  8775  nneneq  8896  onfin2  8945  dif1enALT  8980  unfilem1  9008  rankwflemb  9482  sornom  9964  isf32lem9  10048  axdc3lem2  10138  axdc4lem  10142  zorn2lem3  10185  zorn2lem7  10189  tskuni  10470  grur1a  10506  grothomex  10516  genpnnp  10692  ltaddpr  10721  reclem4pr  10737  supadd  11873  supmullem1  11875  uzin  12547  elfzmlbp  13296  isfinite4  14005  brfi1uzind  14140  swrdnd  14295  sqrlem6  14887  sqreulem  14999  fvprmselgcd1  16674  lubun  18148  lspsneq  20299  fvmptnn04ifb  21908  fbasfip  22927  alexsubALTlem2  23107  ovolunlem1  24566  dchrisum0flb  26563  brbtwn2  27176  axcontlem8  27242  isclwwlknx  28301  clwwlkel  28311  clwwlknwwlksnb  28320  wwlksext2clwwlk  28322  mdbr3  30560  mdbr4  30561  atssma  30641  atcvatlem  30648  ssrelf  30856  fnrelpredd  32961  nepss  33564  sotr3  33639  nodmon  33780  noextendseq  33797  nocvxminlem  33899  hfun  34407  bj-ax12ig  34744  bj-substw  34831  finxpreclem2  35488  indexdom  35819  fdc  35830  totbndss  35862  grpomndo  35960  iss2  36406  ax12eq  36882  ax12el  36883  lsatn0  36940  lsatcmp  36944  lsatcv0  36972  lfl1dim  37062  lfl1dim2N  37063  lkrss2N  37110  lub0N  37130  glb0N  37134  ispsubcl2N  37888  cdlemefrs29bpre0  38337  dihglblem2N  39235  dihglblem3N  39236  dochsnnz  39391  pm13.14  41916  tratrb  42045  ax6e2ndeq  42068  3impexpbicomVD  42366  tratrbVD  42370  equncomVD  42377  trsbcVD  42386  sbcssgVD  42392  csbingVD  42393  onfrALTVD  42400  csbsngVD  42402  csbxpgVD  42403  csbresgVD  42404  csbrngVD  42405  csbima12gALTVD  42406  csbunigVD  42407  csbfv12gALTVD  42408  con5VD  42409  hbimpgVD  42413  hbexgVD  42415  ax6e2ndeqVD  42418  supxrleubrnmpt  42836  suprleubrnmpt  42852  infxrgelbrnmpt  42884  isassintop  45292  zgtp1leeq  45750