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  686  biorf  745  biorfi  747  pm4.72  828  con34bdc  872  notnotbdc  873  dfandc  885  imanst  889  dfordc  893  dfor2dc  896  pm4.79dc  904  orimdidc  907  pm5.54dc  919  pm5.62dc  947  bimsc1  965  modc  2096  euan  2109  exmoeudc  2116  nebidc  2455  cgsexg  2806  cgsex2g  2807  cgsex4g  2808  elab3gf  2922  abidnf  2940  elsn2g  3665  difsn  3769  prel12  3811  dfnfc2  3867  intmin4  3912  dfiin2g  3959  elpw2g  4199  ordsucg  4549  ssrel  4762  ssrel2  4764  ssrelrel  4774  releldmb  4914  relelrnb  4915  cnveqb  5137  dmsnopg  5153  relcnvtr  5201  relcnvexb  5221  f1ocnvb  5535  ffvresb  5742  fconstfvm  5801  fnoprabg  6045  dfsmo2  6372  nntri2  6579  nntri1  6581  en1bg  6891  pw2f1odclem  6930  fieq0  7077  djulclb  7156  ismkvnex  7256  nngt1ne1  9070  znegclb  9404  iccneg  10110  fzsn  10187  fz1sbc  10217  fzofzp1b  10355  ceilqidz  10459  flqeqceilz  10461  reim0b  11115  rexanre  11473  dvdsext  12108  zob  12144  pc11  12596  pcz  12597  gsumval2  13171  issubg2m  13467  issubg4m  13471  ghmmhmb  13532  opprrngbg  13782  opprringbg  13784  issubrng2  13914  issubrg2  13945  eltg3  14471  bastop  14489  cnptoprest  14653  cos11  15267  zabsle1  15418  lgsabs1  15458  lgsquadlem2  15497  bj-om  15806