Theorem impbid2 131

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

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biimt  230  mtt  610  biorf  663  biorfi  665  pm4.72  736  biort  738  con34bdc  765  notnotbdc  766  dfandc  778  dfordc  791  dfor2dc  794  pm4.79dc  809  orimdidc  812  pm5.54dc  827  pm5.62dc  852  bimsc1  870  modc  1943  euan  1956  exmoeudc  1963  nebidc  2285  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  elab3gf  2692  abidnf  2709  elsn2g  3404  difsn  3501  prel12  3542  dfnfc2  3598  intmin4  3643  dfiin2g  3690  elpw2g  3910  ordsucg  4228  ssrel  4428  ssrel2  4430  ssrelrel  4440  releldmb  4571  relelrnb  4572  cnveqb  4776  dmsnopg  4792  relcnvtr  4840  relcnvexb  4857  f1ocnvb  5140  ffvresb  5328  fconstfvm  5379  fnoprabg  5602  dfsmo2  5902  nntri2  6073  nntri1  6074  en1bg  6280  nngt1ne1  7948  znegclb  8278  iccneg  8857  fzsn  8929  fz1sbc  8958  fzofzp1b  9084  ceilqidz  9158  flqeqceilz  9160  reim0b  9462  bj-om  10061