Theorem impbid2 142

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 141	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
4	3	bicomd 140	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimt  240  mtt  675  biorf  734  biorfi  736  pm4.72  813  biort  815  con34bdc  857  notnotbdc  858  dfandc  870  imanst  874  dfordc  878  dfor2dc  881  pm4.79dc  889  orimdidc  892  pm5.54dc  904  pm5.62dc  930  bimsc1  948  modc  2043  euan  2056  exmoeudc  2063  nebidc  2389  cgsexg  2724  cgsex2g  2725  cgsex4g  2726  elab3gf  2838  abidnf  2856  elsn2g  3565  difsn  3665  prel12  3706  dfnfc2  3762  intmin4  3807  dfiin2g  3854  elpw2g  4089  ordsucg  4426  ssrel  4635  ssrel2  4637  ssrelrel  4647  releldmb  4784  relelrnb  4785  cnveqb  5002  dmsnopg  5018  relcnvtr  5066  relcnvexb  5086  f1ocnvb  5389  ffvresb  5591  fconstfvm  5646  fnoprabg  5880  dfsmo2  6192  nntri2  6398  nntri1  6400  en1bg  6702  fieq0  6872  djulclb  6948  ismkvnex  7037  nngt1ne1  8779  znegclb  9111  iccneg  9802  fzsn  9877  fz1sbc  9907  fzofzp1b  10036  ceilqidz  10120  flqeqceilz  10122  reim0b  10666  rexanre  11024  dvdsext  11589  zob  11624  eltg3  12265  bastop  12283  cnptoprest  12447  cos11  12982  bj-om  13306