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  692  biorf  752  biorfi  754  pm4.72  835  con34bdc  879  notnotbdc  880  dfandc  892  imanst  896  dfordc  900  dfor2dc  903  pm4.79dc  911  orimdidc  914  pm5.54dc  926  pm5.62dc  954  bimsc1  972  dfifp2dc  990  modc  2123  euan  2136  exmoeudc  2143  nebidc  2483  cgsexg  2839  cgsex2g  2840  cgsex4g  2841  elab3gf  2957  abidnf  2975  elsn2g  3706  difsn  3815  prel12  3859  dfnfc2  3916  intmin4  3961  dfiin2g  4008  elpw2g  4251  ordsucg  4606  ssrel  4820  ssrel2  4822  ssrelrel  4832  releldmb  4975  relelrnb  4976  cnveqb  5199  dmsnopg  5215  relcnvtr  5263  relcnvexb  5283  f1ocnvb  5606  ffvresb  5818  fconstfvm  5880  fnoprabg  6132  dfsmo2  6496  nntri2  6705  nntri1  6707  en1bg  7017  pw2f1odclem  7063  fieq0  7218  djulclb  7297  ismkvnex  7397  nngt1ne1  9220  znegclb  9556  iccneg  10268  fzsn  10346  fz1sbc  10376  fzofzp1b  10519  ceilqidz  10624  flqeqceilz  10626  reim0b  11485  rexanre  11843  dvdsext  12479  zob  12515  pc11  12967  pcz  12968  gsumval2  13543  issubg2m  13839  issubg4m  13843  ghmmhmb  13904  opprrngbg  14155  opprringbg  14157  issubrng2  14288  issubrg2  14319  eltg3  14851  bastop  14869  cnptoprest  15033  cos11  15647  zabsle1  15801  lgsabs1  15841  lgsquadlem2  15880  issubgr2  16182  uhgrissubgr  16185  clwwlknun  16365  bj-om  16636  qdiff  16764