Theorem biimprcd 252

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  biimparc  482  ax12i  1968  moanimlem  2702  euan  2705  euanv  2708  eleq1a  2911  ceqsalgALT  3533  cgsexg  3540  cgsex2g  3541  cgsex4g  3542  ceqsex  3543  spcegv  3600  spc2egv  3603  reu6  3720  csbiebt  3915  dfiin2g  4960  reusv2lem2  5303  ralxfrALT  5319  opelxp  5594  ssrel  5660  ssrel2  5662  ssrelrel  5672  iss  5906  ordun  6295  fprb  6959  riotaclb  7158  iunpw  7496  limom  7598  funcnvuni  7639  fiunlem  7646  soxp  7826  tfrlem8  8023  oaordex  8187  eroveu  8395  fundmen  8586  nneneq  8703  onfin2  8713  dif1en  8754  unfilem1  8785  rankwflemb  9225  sornom  9702  isf32lem9  9786  axdc3lem2  9876  axdc4lem  9880  zorn2lem3  9923  zorn2lem7  9927  tskuni  10208  grur1a  10244  grothomex  10254  genpnnp  10430  ltaddpr  10459  reclem4pr  10475  supadd  11612  supmullem1  11614  uzin  12281  elfzmlbp  13021  isfinite4  13726  brfi1uzind  13859  swrdnd  14019  sqrlem6  14610  sqreulem  14722  fvprmselgcd1  16384  lubun  17736  lspsneq  19897  fvmptnn04ifb  21462  fbasfip  22479  alexsubALTlem2  22659  ovolunlem1  24101  dchrisum0flb  26089  brbtwn2  26694  axcontlem8  26760  isclwwlknx  27817  clwwlkel  27828  clwwlknwwlksnb  27837  wwlksext2clwwlk  27839  mdbr3  30077  mdbr4  30078  atssma  30158  atcvatlem  30165  ssrelf  30369  nepss  32952  sotr3  33006  nodmon  33161  noextendseq  33178  nocvxminlem  33251  hfun  33643  bj-ax12ig  33973  finxpreclem2  34675  indexdom  35013  fdc  35024  totbndss  35059  grpomndo  35157  iss2  35605  ax12eq  36081  ax12el  36082  lsatn0  36139  lsatcmp  36143  lsatcv0  36171  lfl1dim  36261  lfl1dim2N  36262  lkrss2N  36309  lub0N  36329  glb0N  36333  ispsubcl2N  37087  cdlemefrs29bpre0  37536  dihglblem2N  38434  dihglblem3N  38435  dochsnnz  38590  pm13.14  40747  tratrb  40876  ax6e2ndeq  40899  3impexpbicomVD  41197  tratrbVD  41201  equncomVD  41208  trsbcVD  41217  sbcssgVD  41223  csbingVD  41224  onfrALTVD  41231  csbsngVD  41233  csbxpgVD  41234  csbresgVD  41235  csbrngVD  41236  csbima12gALTVD  41237  csbunigVD  41238  csbfv12gALTVD  41239  con5VD  41240  hbimpgVD  41244  hbexgVD  41246  ax6e2ndeqVD  41249  supxrleubrnmpt  41685  suprleubrnmpt  41702  infxrgelbrnmpt  41736  isassintop  44124  zgtp1leeq  44583