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  1966  moanimlem  2618  euan  2621  euanv  2624  eleq1a  2836  ceqsalgALT  3518  cgsexg  3526  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  ceqsexOLD  3531  spcegv  3597  spc2egv  3599  reu6  3732  csbiebt  3928  dfiin2g  5032  reusv2lem2  5399  ralxfrALT  5415  axprlem4  5426  sotr3  5633  opelxp  5721  ssrel  5792  ssrelOLD  5793  ssrel2  5795  ssrelrel  5806  iss  6053  ordun  6488  fprb  7214  riotaclb  7429  iunpw  7791  limom  7903  funcnvuni  7954  fiunlem  7966  soxp  8154  tfrlem8  8424  oaordex  8596  eroveu  8852  fundmen  9071  nneneq  9246  nneneqOLD  9258  onfin2  9268  dif1ennnALT  9311  unfilem1  9343  rankwflemb  9833  sornom  10317  isf32lem9  10401  axdc3lem2  10491  axdc4lem  10495  zorn2lem3  10538  zorn2lem7  10542  tskuni  10823  grur1a  10859  grothomex  10869  genpnnp  11045  ltaddpr  11074  reclem4pr  11090  supadd  12236  supmullem1  12238  uzin  12918  elfzmlbp  13679  isfinite4  14401  brfi1uzind  14547  swrdnd  14692  01sqrexlem6  15286  sqreulem  15398  fvprmselgcd1  17083  lubun  18560  lspsneq  21124  fvmptnn04ifb  22857  fbasfip  23876  alexsubALTlem2  24056  ovolunlem1  25532  dchrisum0flb  27554  nodmon  27695  noextendseq  27712  nocvxminlem  27822  brbtwn2  28920  axcontlem8  28986  isclwwlknx  30055  clwwlkel  30065  clwwlknwwlksnb  30074  wwlksext2clwwlk  30076  mdbr3  32316  mdbr4  32317  atssma  32397  atcvatlem  32404  ssrelf  32627  fnrelpredd  35103  nepss  35718  hfun  36179  bj-ax12ig  36637  bj-substw  36723  finxpreclem2  37391  indexdom  37741  fdc  37752  totbndss  37784  grpomndo  37882  iss2  38345  ax12eq  38942  ax12el  38943  lsatn0  39000  lsatcmp  39004  lsatcv0  39032  lfl1dim  39122  lfl1dim2N  39123  lkrss2N  39170  lub0N  39190  glb0N  39194  ispsubcl2N  39949  cdlemefrs29bpre0  40398  dihglblem2N  41296  dihglblem3N  41297  dochsnnz  41452  pm13.14  44428  tratrb  44556  ax6e2ndeq  44579  3impexpbicomVD  44877  tratrbVD  44881  equncomVD  44888  trsbcVD  44897  sbcssgVD  44903  csbingVD  44904  onfrALTVD  44911  csbsngVD  44913  csbxpgVD  44914  csbresgVD  44915  csbrngVD  44916  csbima12gALTVD  44917  csbunigVD  44918  csbfv12gALTVD  44919  con5VD  44920  hbimpgVD  44924  hbexgVD  44926  ax6e2ndeqVD  44929  supxrleubrnmpt  45417  suprleubrnmpt  45433  infxrgelbrnmpt  45465  usgrgrtrirex  47917  isassintop  48126  zgtp1leeq  48438