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  1969  moanimlem  2703  euan  2706  euanv  2709  eleq1a  2910  ceqsalgALT  3532  cgsexg  3539  cgsex2g  3540  cgsex4g  3541  ceqsex  3542  spcegv  3599  spc2egv  3602  reu6  3719  csbiebt  3914  dfiin2g  4959  reusv2lem2  5302  ralxfrALT  5318  opelxp  5593  ssrel  5659  ssrel2  5661  ssrelrel  5671  iss  5905  ordun  6294  fprb  6958  riotaclb  7157  iunpw  7495  limom  7597  funcnvuni  7638  fiunlem  7645  soxp  7825  tfrlem8  8022  oaordex  8186  eroveu  8394  fundmen  8585  nneneq  8702  onfin2  8712  dif1en  8753  unfilem1  8784  rankwflemb  9224  sornom  9701  isf32lem9  9785  axdc3lem2  9875  axdc4lem  9879  zorn2lem3  9922  zorn2lem7  9926  tskuni  10207  grur1a  10243  grothomex  10253  genpnnp  10429  ltaddpr  10458  reclem4pr  10474  supadd  11611  supmullem1  11613  uzin  12281  elfzmlbp  13021  isfinite4  13726  brfi1uzind  13859  swrdnd  14018  sqrlem6  14609  sqreulem  14721  fvprmselgcd1  16383  lubun  17735  lspsneq  19896  fvmptnn04ifb  21461  fbasfip  22478  alexsubALTlem2  22658  ovolunlem1  24100  dchrisum0flb  26088  brbtwn2  26693  axcontlem8  26759  isclwwlknx  27816  clwwlkel  27827  clwwlknwwlksnb  27836  wwlksext2clwwlk  27838  mdbr3  30076  mdbr4  30077  atssma  30157  atcvatlem  30164  ssrelf  30368  nepss  32950  sotr3  33004  nodmon  33159  noextendseq  33176  nocvxminlem  33249  hfun  33641  bj-ax12ig  33971  finxpreclem2  34673  indexdom  35011  fdc  35022  totbndss  35057  grpomndo  35155  iss2  35603  ax12eq  36079  ax12el  36080  lsatn0  36137  lsatcmp  36141  lsatcv0  36169  lfl1dim  36259  lfl1dim2N  36260  lkrss2N  36307  lub0N  36327  glb0N  36331  ispsubcl2N  37085  cdlemefrs29bpre0  37534  dihglblem2N  38432  dihglblem3N  38433  dochsnnz  38588  pm13.14  40748  tratrb  40877  ax6e2ndeq  40900  3impexpbicomVD  41198  tratrbVD  41202  equncomVD  41209  trsbcVD  41218  sbcssgVD  41224  csbingVD  41225  onfrALTVD  41232  csbsngVD  41234  csbxpgVD  41235  csbresgVD  41236  csbrngVD  41237  csbima12gALTVD  41238  csbunigVD  41239  csbfv12gALTVD  41240  con5VD  41241  hbimpgVD  41245  hbexgVD  41247  ax6e2ndeqVD  41250  supxrleubrnmpt  41686  suprleubrnmpt  41703  infxrgelbrnmpt  41737  isassintop  44124  zgtp1leeq  44583