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  609  biorf  662  biorfi  664  pm4.72  735  biort  737  con34bdc  764  notnotdc  765  dfandc  777  dfordc  790  dfor2dc  793  pm4.79dc  808  orimdidc  811  pm5.54dc  826  pm5.62dc  851  bimsc1  869  modc  1940  euan  1953  exmoeudc  1960  nebidc  2279  cgsexg  2583  cgsex2g  2584  cgsex4g  2585  elab3gf  2686  abidnf  2703  elsnc2g  3396  difsn  3492  prel12  3533  dfnfc2  3589  intmin4  3634  dfiin2g  3681  elpw2g  3901  ordsucg  4194  ssrel  4371  ssrel2  4373  ssrelrel  4383  releldmb  4514  relelrnb  4515  cnveqb  4719  dmsnopg  4735  relcnvtr  4783  relcnvexb  4800  f1ocnvb  5083  ffvresb  5271  fconstfvm  5322  fnoprabg  5544  dfsmo2  5843  nntri2  6012  nntri1  6013  en1bg  6216  nngt1ne1  7709  znegclb  8034  iccneg  8607  fzsn  8679  fz1sbc  8708  fzofzp1b  8834  reim0b  9070  bj-om  9371