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  5872  fnoprabg  6122  dfsmo2  6453  nntri2  6662  nntri1  6664  en1bg  6974  pw2f1odclem  7020  fieq0  7175  djulclb  7254  ismkvnex  7354  nngt1ne1  9178  znegclb  9512  iccneg  10224  fzsn  10301  fz1sbc  10331  fzofzp1b  10474  ceilqidz  10579  flqeqceilz  10581  reim0b  11427  rexanre  11785  dvdsext  12421  zob  12457  pc11  12909  pcz  12910  gsumval2  13485  issubg2m  13781  issubg4m  13785  ghmmhmb  13846  opprrngbg  14097  opprringbg  14099  issubrng2  14230  issubrg2  14261  eltg3  14787  bastop  14805  cnptoprest  14969  cos11  15583  zabsle1  15734  lgsabs1  15774  lgsquadlem2  15813  issubgr2  16115  uhgrissubgr  16118  clwwlknun  16298  bj-om  16558  qdiff  16679