Theorem biimprcd 249

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  biimparc  478  ax12i  1968  moanimlem  2612  euan  2615  euanv  2618  eleq1a  2826  ceqsalgALT  3507  cgsexg  3517  cgsex2g  3518  cgsex4g  3519  cgsex4gOLD  3520  cgsex4gOLDOLD  3521  ceqsexOLD  3523  ceqsexvOLD  3525  spcegv  3586  spc2egv  3588  reu6  3721  csbiebt  3922  dfiin2g  5034  reusv2lem2  5396  ralxfrALT  5412  sotr3  5626  opelxp  5711  ssrel  5781  ssrelOLD  5782  ssrel2  5784  ssrelrel  5795  iss  6034  ordun  6467  fprb  7196  riotaclb  7409  iunpw  7760  limom  7873  funcnvuni  7924  fiunlem  7930  soxp  8117  tfrlem8  8386  oaordex  8560  eroveu  8808  fundmen  9033  nneneq  9211  nneneqOLD  9223  onfin2  9233  dif1ennnALT  9279  unfilem1  9312  rankwflemb  9790  sornom  10274  isf32lem9  10358  axdc3lem2  10448  axdc4lem  10452  zorn2lem3  10495  zorn2lem7  10499  tskuni  10780  grur1a  10816  grothomex  10826  genpnnp  11002  ltaddpr  11031  reclem4pr  11047  supadd  12186  supmullem1  12188  uzin  12866  elfzmlbp  13616  isfinite4  14326  brfi1uzind  14463  swrdnd  14608  01sqrexlem6  15198  sqreulem  15310  fvprmselgcd1  16982  lubun  18472  lspsneq  20880  fvmptnn04ifb  22573  fbasfip  23592  alexsubALTlem2  23772  ovolunlem1  25246  dchrisum0flb  27249  nodmon  27389  noextendseq  27406  nocvxminlem  27515  brbtwn2  28430  axcontlem8  28496  isclwwlknx  29556  clwwlkel  29566  clwwlknwwlksnb  29575  wwlksext2clwwlk  29577  mdbr3  31817  mdbr4  31818  atssma  31898  atcvatlem  31905  ssrelf  32111  fnrelpredd  34390  nepss  34991  hfun  35454  bj-ax12ig  35816  bj-substw  35903  finxpreclem2  36574  indexdom  36905  fdc  36916  totbndss  36948  grpomndo  37046  iss2  37516  ax12eq  38114  ax12el  38115  lsatn0  38172  lsatcmp  38176  lsatcv0  38204  lfl1dim  38294  lfl1dim2N  38295  lkrss2N  38342  lub0N  38362  glb0N  38366  ispsubcl2N  39121  cdlemefrs29bpre0  39570  dihglblem2N  40468  dihglblem3N  40469  dochsnnz  40624  pm13.14  43470  tratrb  43599  ax6e2ndeq  43622  3impexpbicomVD  43920  tratrbVD  43924  equncomVD  43931  trsbcVD  43940  sbcssgVD  43946  csbingVD  43947  onfrALTVD  43954  csbsngVD  43956  csbxpgVD  43957  csbresgVD  43958  csbrngVD  43959  csbima12gALTVD  43960  csbunigVD  43961  csbfv12gALTVD  43962  con5VD  43963  hbimpgVD  43967  hbexgVD  43969  ax6e2ndeqVD  43972  supxrleubrnmpt  44414  suprleubrnmpt  44430  infxrgelbrnmpt  44462  isassintop  46886  zgtp1leeq  47289