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  11144  rexanre  11502  dvdsext  12137  zob  12173  pc11  12625  pcz  12626  gsumval2  13200  issubg2m  13496  issubg4m  13500  ghmmhmb  13561  opprrngbg  13811  opprringbg  13813  issubrng2  13943  issubrg2  13974  eltg3  14500  bastop  14518  cnptoprest  14682  cos11  15296  zabsle1  15447  lgsabs1  15487  lgsquadlem2  15526  bj-om  15835