Theorem impbid2 143

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)

Hypotheses

Ref	Expression
impbid2.1	⊢ (𝜓 → 𝜒)
impbid2.2	⊢ (𝜑 → (𝜒 → 𝜓))

Assertion

Ref	Expression
impbid2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid2

Step	Hyp	Ref	Expression
1		impbid2.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
2		impbid2.1	. . 3 ⊢ (𝜓 → 𝜒)
3	1, 2	impbid1 142	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 141	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimt  241  mtt  691  biorf  751  biorfi  753  pm4.72  834  con34bdc  878  notnotbdc  879  dfandc  891  imanst  895  dfordc  899  dfor2dc  902  pm4.79dc  910  orimdidc  913  pm5.54dc  925  pm5.62dc  953  bimsc1  971  dfifp2dc  989  modc  2123  euan  2136  exmoeudc  2143  nebidc  2482  cgsexg  2838  cgsex2g  2839  cgsex4g  2840  elab3gf  2956  abidnf  2974  elsn2g  3702  difsn  3810  prel12  3854  dfnfc2  3911  intmin4  3956  dfiin2g  4003  elpw2g  4246  ordsucg  4600  ssrel  4814  ssrel2  4816  ssrelrel  4826  releldmb  4969  relelrnb  4970  cnveqb  5192  dmsnopg  5208  relcnvtr  5256  relcnvexb  5276  f1ocnvb  5597  ffvresb  5810  fconstfvm  5871  fnoprabg  6121  dfsmo2  6452  nntri2  6661  nntri1  6663  en1bg  6973  pw2f1odclem  7019  fieq0  7174  djulclb  7253  ismkvnex  7353  nngt1ne1  9177  znegclb  9511  iccneg  10223  fzsn  10300  fz1sbc  10330  fzofzp1b  10472  ceilqidz  10577  flqeqceilz  10579  reim0b  11422  rexanre  11780  dvdsext  12415  zob  12451  pc11  12903  pcz  12904  gsumval2  13479  issubg2m  13775  issubg4m  13779  ghmmhmb  13840  opprrngbg  14090  opprringbg  14092  issubrng2  14223  issubrg2  14254  eltg3  14780  bastop  14798  cnptoprest  14962  cos11  15576  zabsle1  15727  lgsabs1  15767  lgsquadlem2  15806  issubgr2  16108  uhgrissubgr  16111  clwwlknun  16291  bj-om  16532