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 23	. 2 ⊢ (𝜒 → 𝜒)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibrcom 250	1 ⊢ (𝜒 → (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimparc  485  ax12i  1999  moanimlem  2644  euan  2647  euanv  2650  eleq1a  2856  ceqsalgALT  3487  cgsexg  3495  cgsex2g  3496  cgsex4g  3497  spcegv  3552  spc2egv  3554  reu6  3684  csbiebt  3876  reusv2lem2  5361  ralxfrALT  5377  axprlem4  5388  sotr3  5600  opelxp  5687  ssrel  5759  ssrel2  5761  ssrelrel  5772  iss  6027  ordun  6470  fprb  7200  riotaclb  7419  iunpw  7786  limom  7894  funcnvuni  7945  fiunlem  7955  soxp  8142  tfrlem8  8393  oaordex  8567  eroveu  8834  fundmen  9060  nneneq  9222  onfin2  9233  dif1ennnALT  9269  unfilem1  9298  elirrv  9592  rankwflemb  9801  rankwflembOLD  9802  hfunOLD  9920  sornom  10356  isf32lem9  10440  axdc3lem2  10530  axdc4lem  10534  zorn2lem3  10577  zorn2lem7  10581  tskuni  10869  grur1a  10905  grothomex  10915  genpnnp  11091  ltaddpr  11120  reclem4pr  11136  supadd  12286  supmullem1  12288  uzin  13002  elfzmlbp  13774  isfinite4  14507  brfi1uzind  14654  swrdnd  14805  01sqrexlem6  15415  sqreulem  15528  fvprmselgcd1  17224  lubun  18690  lspsneq  21401  fvmptnn04ifb  23170  fbasfip  24188  alexsubALTlem2  24368  ovolunlem1  25819  dchrisum0flb  27838  nodmon  28008  noextendseq  28025  nocvxminlem  28141  brbtwn2  29484  axcontlem8  29550  isclwwlknx  30628  clwwlkel  30638  clwwlknwwlksnb  30647  wwlksext2clwwlk  30649  mdbr3  32900  mdbr4  32901  atssma  32981  atcvatlem  32988  ssrelf  33210  fnrelpredd  35721  nepss  36484  nmulprop  36940  axtco2  37263  axtcond  37267  bj-ax12ig  37521  bj-alextruim  37537  bj-substw  37628  bj-axreprepsep  37992  finxpreclem2  38315  wl-eujustlem1  38522  indexdom  38670  fdc  38681  totbndss  38713  grpomndo  38811  iss2  39278  ax12eq  40000  ax12el  40001  lsatn0  40058  lsatcmp  40062  lsatcv0  40090  lfl1dim  40180  lfl1dim2N  40181  lkrss2N  40228  lub0N  40248  glb0N  40252  ispsubcl2N  41006  cdlemefrs29bpre0  41455  dihglblem2N  42353  dihglblem3N  42354  dochsnnz  42509  pm13.14  45394  tratrb  45520  ax6e2ndeq  45543  3impexpbicomVD  45840  tratrbVD  45844  equncomVD  45851  trsbcVD  45860  sbcssgVD  45866  csbingVD  45867  onfrALTVD  45874  csbsngVD  45876  csbxpgVD  45877  csbresgVD  45878  csbrngVD  45879  csbima12gALTVD  45880  csbunigVD  45881  csbfv12gALTVD  45882  con5VD  45883  hbimpgVD  45887  hbexgVD  45889  ax6e2ndeqVD  45892  supxrleubrnmpt  46417  suprleubrnmpt  46433  infxrgelbrnmpt  46465  usgrgrtrirex  49049  isassintop  49308  zgtp1leeq  49634