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  2124  euan  2137  exmoeudc  2144  nebidc  2492  cgsexg  2849  cgsex2g  2850  cgsex4g  2851  elab3gf  2967  abidnf  2985  elsn2g  3722  difsn  3831  prel12  3875  dfnfc2  3932  intmin4  3977  dfiin2g  4024  elpw2g  4268  ordsucg  4624  ssrel  4838  ssrel2  4840  ssrelrel  4850  releldmb  4994  relelrnb  4995  cnveqb  5218  dmsnopg  5234  relcnvtr  5282  relcnvexb  5302  f1ocnvb  5628  ffvresb  5840  fconstfvm  5902  fnoprabg  6154  dfsmo2  6518  nntri2  6727  nntri1  6729  en1bg  7040  pw2f1odclem  7087  fieq0  7263  djulclb  7346  ismkvnex  7446  nngt1ne1  9272  znegclb  9610  iccneg  10322  fzsn  10400  fz1sbc  10430  fzofzp1b  10573  ceilqidz  10678  flqeqceilz  10680  reim0b  11547  rexanre  11905  dvdsext  12541  zob  12577  pc11  13029  pcz  13030  gsumval2  13610  issubg2m  13906  issubg4m  13910  ghmmhmb  13971  opprrngbg  14222  opprringbg  14224  issubrng2  14355  issubrg2  14386  aprlring  14434  eltg3  14922  bastop  14940  cnptoprest  15104  cos11  15718  zabsle1  15872  lgsabs1  15912  lgsquadlem2  15951  issubgr2  16253  uhgrissubgr  16256  clwwlknun  16436  bj-om  16707  qdiff  16833