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  946  bimsc1  964  modc  2079  euan  2092  exmoeudc  2099  nebidc  2437  cgsexg  2784  cgsex2g  2785  cgsex4g  2786  elab3gf  2899  abidnf  2917  elsn2g  3637  difsn  3741  prel12  3783  dfnfc2  3839  intmin4  3884  dfiin2g  3931  elpw2g  4168  ordsucg  4513  ssrel  4726  ssrel2  4728  ssrelrel  4738  releldmb  4876  relelrnb  4877  cnveqb  5096  dmsnopg  5112  relcnvtr  5160  relcnvexb  5180  f1ocnvb  5487  ffvresb  5692  fconstfvm  5747  fnoprabg  5989  dfsmo2  6302  nntri2  6509  nntri1  6511  en1bg  6814  fieq0  6989  djulclb  7068  ismkvnex  7167  nngt1ne1  8968  znegclb  9300  iccneg  10003  fzsn  10080  fz1sbc  10110  fzofzp1b  10242  ceilqidz  10330  flqeqceilz  10332  reim0b  10885  rexanre  11243  dvdsext  11875  zob  11910  pc11  12344  pcz  12345  issubg2m  13081  issubg4m  13085  opprrngbg  13326  opprringbg  13328  issubrng2  13430  issubrg2  13461  eltg3  13853  bastop  13871  cnptoprest  14035  cos11  14570  zabsle1  14696  lgsabs1  14736  bj-om  14985