Theorem biimprcd 241

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  biimparc  471  ax12i  2061  moanim  2651  euan  2652  eleq1a  2839  ceqsalgALT  3384  cgsexg  3391  cgsex2g  3392  cgsex4g  3393  ceqsex  3394  spc2egv  3448  spc3egv  3450  reu6  3556  csbiebt  3713  dfiin2g  4711  reusv2lem2  5036  ralxfrALT  5052  opelxp  5315  ssrel  5379  ssrel2  5381  ssrelrel  5391  iss  5626  ordun  6011  riotaclb  6845  iunpw  7180  limom  7282  funcnvuni  7321  fun11iun  7328  soxp  7496  tfrlem8  7688  oaordex  7847  eroveu  8050  fundmen  8238  nneneq  8354  onfin2  8363  dif1en  8404  unfilem1  8435  rankwflemb  8875  sornom  9356  isf32lem9  9440  axdc3lem2  9530  axdc4lem  9534  zorn2lem3  9577  zorn2lem7  9581  tskuni  9862  grur1a  9898  grothomex  9908  genpnnp  10084  ltaddpr  10113  reclem4pr  10129  supadd  11249  supmullem1  11251  uzin  11925  elfzmlbp  12663  isfinite4  13360  brfi1uzind  13486  swrdnd  13641  sqrlem6  14287  sqreulem  14398  fvprmselgcd1  16042  lubun  17403  lspsneq  19408  fvmptnn04ifb  20949  fbasfip  21965  alexsubALTlem2  22145  ovolunlem1  23569  dchrisum0flb  25504  brbtwn2  26090  axcontlem8  26156  isclwwlknx  27295  clwwlknwwlksnb  27323  mdbr3  29633  mdbr4  29634  atssma  29714  atcvatlem  29721  ssrelf  29896  nepss  32066  sotr3  32122  fprb  32135  nodmon  32268  noextendseq  32285  nocvxminlem  32358  hfun  32750  bj-ax12ig  33072  finxpreclem2  33681  indexdom  33973  fdc  33984  totbndss  34019  grpomndo  34117  iss2  34562  ax12eq  34918  ax12el  34919  lsatn0  34976  lsatcmp  34980  lsatcv0  35008  lfl1dim  35098  lfl1dim2N  35099  lkrss2N  35146  lub0N  35166  glb0N  35170  ispsubcl2N  35924  cdlemefrs29bpre0  36373  dihglblem2N  37271  dihglblem3N  37272  dochsnnz  37427  pm13.14  39307  tratrb  39438  ax6e2ndeq  39461  3impexpbicomVD  39769  tratrbVD  39773  equncomVD  39780  trsbcVD  39789  sbcssgVD  39795  csbingVD  39796  onfrALTVD  39803  csbsngVD  39805  csbxpgVD  39806  csbresgVD  39807  csbrngVD  39808  csbima12gALTVD  39809  csbunigVD  39810  csbfv12gALTVD  39811  con5VD  39812  hbimpgVD  39816  hbexgVD  39818  ax6e2ndeqVD  39821  supxrleubrnmpt  40293  suprleubrnmpt  40310  infxrgelbrnmpt  40344  isassintop  42539  zgtp1leeq  43004