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  2645  euan  2648  euanv  2651  eleq1a  2857  ceqsalgALT  3489  cgsexg  3497  cgsex2g  3498  cgsex4g  3499  spcegv  3554  spc2egv  3556  reu6  3687  csbiebt  3879  reusv2lem2  5368  ralxfrALT  5384  axprlem4  5395  sotr3  5608  opelxp  5695  ssrel  5767  ssrel2  5769  ssrelrel  5780  iss  6035  ordun  6468  fprb  7195  riotaclb  7414  iunpw  7773  limom  7881  funcnvuni  7932  fiunlem  7942  soxp  8130  tfrlem8  8376  oaordex  8548  eroveu  8815  fundmen  9041  nneneq  9203  onfin2  9214  dif1ennnALT  9250  unfilem1  9278  elirrv  9572  rankwflemb  9778  sornom  10282  isf32lem9  10366  axdc3lem2  10456  axdc4lem  10460  zorn2lem3  10503  zorn2lem7  10507  tskuni  10795  grur1a  10831  grothomex  10841  genpnnp  11017  ltaddpr  11046  reclem4pr  11062  supadd  12210  supmullem1  12212  uzin  12926  elfzmlbp  13696  isfinite4  14428  brfi1uzind  14575  swrdnd  14726  01sqrexlem6  15336  sqreulem  15449  fvprmselgcd1  17141  lubun  18607  lspsneq  21310  fvmptnn04ifb  23077  fbasfip  24095  alexsubALTlem2  24275  ovolunlem1  25726  dchrisum0flb  27744  nodmon  27884  noextendseq  27901  nocvxminlem  28017  brbtwn2  29348  axcontlem8  29414  isclwwlknx  30492  clwwlkel  30502  clwwlknwwlksnb  30511  wwlksext2clwwlk  30513  mdbr3  32764  mdbr4  32765  atssma  32845  atcvatlem  32852  ssrelf  33075  fnrelpredd  35583  nepss  36284  hfun  36745  nmulprop  36757  axtco2  37080  axtcond  37084  bj-ax12ig  37338  bj-alextruim  37354  bj-substw  37445  bj-axreprepsep  37807  finxpreclem2  38131  wl-eujustlem1  38338  indexdom  38471  fdc  38482  totbndss  38514  grpomndo  38612  iss2  39079  ax12eq  39801  ax12el  39802  lsatn0  39859  lsatcmp  39863  lsatcv0  39891  lfl1dim  39981  lfl1dim2N  39982  lkrss2N  40029  lub0N  40049  glb0N  40053  ispsubcl2N  40807  cdlemefrs29bpre0  41256  dihglblem2N  42154  dihglblem3N  42155  dochsnnz  42310  pm13.14  45220  tratrb  45346  ax6e2ndeq  45369  3impexpbicomVD  45666  tratrbVD  45670  equncomVD  45677  trsbcVD  45686  sbcssgVD  45692  csbingVD  45693  onfrALTVD  45700  csbsngVD  45702  csbxpgVD  45703  csbresgVD  45704  csbrngVD  45705  csbima12gALTVD  45706  csbunigVD  45707  csbfv12gALTVD  45708  con5VD  45709  hbimpgVD  45713  hbexgVD  45715  ax6e2ndeqVD  45718  supxrleubrnmpt  46221  suprleubrnmpt  46237  infxrgelbrnmpt  46269  usgrgrtrirex  48853  isassintop  49112  zgtp1leeq  49438