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  2126  euan  2139  exmoeudc  2146  nebidc  2494  cgsexg  2851  cgsex2g  2852  cgsex4g  2853  elab3gf  2970  abidnf  2988  elsn2g  3727  difsn  3836  prel12  3880  dfnfc2  3937  intmin4  3982  dfiin2g  4029  elpw2g  4273  ordsucg  4629  ssrel  4843  ssrel2  4845  ssrelrel  4855  releldmb  4999  relelrnb  5000  cnveqb  5223  dmsnopg  5239  relcnvtr  5287  relcnvexb  5307  f1ocnvb  5633  ffvresb  5845  fconstfvm  5907  fnoprabg  6162  dfsmo2  6531  nntri2  6740  nntri1  6742  en1bg  7053  pw2f1odclem  7100  fieq0  7276  djulclb  7359  ismkvnex  7459  nngt1ne1  9289  znegclb  9627  iccneg  10341  fzsn  10421  fz1sbc  10452  fzofzp1b  10595  ceilqidz  10702  flqeqceilz  10704  reim0b  11572  rexanre  11930  dvdsext  12566  zob  12602  pc11  13054  pcz  13055  gsumval2  13660  issubg2m  13942  issubg4m  13946  ghmmhmb  14007  opprrngbg  14321  opprringbg  14323  issubrng2  14456  issubrg2  14487  aprlring  14538  eltg3  15048  bastop  15066  cnptoprest  15230  cos11  15844  zabsle1  15998  lgsabs1  16038  lgsquadlem2  16077  issubgr2  16379  uhgrissubgr  16382  clwwlknun  16562  bj-om  16833  qdiff  16959