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  480  ax12i  1969  moanimlem  2618  euan  2621  euanv  2624  eleq1a  2832  ceqsalgALT  3474  cgsexg  3483  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  ceqsex  3487  ceqsexv  3488  spcegv  3545  spc2egv  3547  reu6  3671  csbiebt  3872  dfiin2g  4976  reusv2lem2  5339  ralxfrALT  5355  sotr3  5565  opelxp  5650  ssrel  5718  ssrelOLD  5719  ssrel2  5721  ssrelrel  5732  iss  5969  ordun  6399  fprb  7119  riotaclb  7328  iunpw  7675  limom  7788  funcnvuni  7838  fiunlem  7844  soxp  8029  tfrlem8  8277  oaordex  8452  eroveu  8664  fundmen  8888  nneneq  9066  nneneqOLD  9078  onfin2  9088  dif1ennnALT  9134  unfilem1  9167  rankwflemb  9642  sornom  10126  isf32lem9  10210  axdc3lem2  10300  axdc4lem  10304  zorn2lem3  10347  zorn2lem7  10351  tskuni  10632  grur1a  10668  grothomex  10678  genpnnp  10854  ltaddpr  10883  reclem4pr  10899  supadd  12036  supmullem1  12038  uzin  12711  elfzmlbp  13460  isfinite4  14169  brfi1uzind  14304  swrdnd  14457  sqrlem6  15050  sqreulem  15162  fvprmselgcd1  16835  lubun  18322  lspsneq  20482  fvmptnn04ifb  22098  fbasfip  23117  alexsubALTlem2  23297  ovolunlem1  24759  dchrisum0flb  26756  nodmon  26896  noextendseq  26913  brbtwn2  27475  axcontlem8  27541  isclwwlknx  28601  clwwlkel  28611  clwwlknwwlksnb  28620  wwlksext2clwwlk  28622  mdbr3  30860  mdbr4  30861  atssma  30941  atcvatlem  30948  ssrelf  31155  fnrelpredd  33273  nepss  33872  nocvxminlem  34063  hfun  34571  bj-ax12ig  34908  bj-substw  34995  finxpreclem2  35659  indexdom  35990  fdc  36001  totbndss  36033  grpomndo  36131  iss2  36603  ax12eq  37201  ax12el  37202  lsatn0  37259  lsatcmp  37263  lsatcv0  37291  lfl1dim  37381  lfl1dim2N  37382  lkrss2N  37429  lub0N  37449  glb0N  37453  ispsubcl2N  38208  cdlemefrs29bpre0  38657  dihglblem2N  39555  dihglblem3N  39556  dochsnnz  39711  pm13.14  42337  tratrb  42466  ax6e2ndeq  42489  3impexpbicomVD  42787  tratrbVD  42791  equncomVD  42798  trsbcVD  42807  sbcssgVD  42813  csbingVD  42814  onfrALTVD  42821  csbsngVD  42823  csbxpgVD  42824  csbresgVD  42825  csbrngVD  42826  csbima12gALTVD  42827  csbunigVD  42828  csbfv12gALTVD  42829  con5VD  42830  hbimpgVD  42834  hbexgVD  42836  ax6e2ndeqVD  42839  supxrleubrnmpt  43270  suprleubrnmpt  43286  infxrgelbrnmpt  43318  isassintop  45744  zgtp1leeq  46202