Theorem impbid2 141

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

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biimt  239  mtt  642  biorf  695  biorfi  697  pm4.72  769  biort  771  con34bdc  798  notnotbdc  799  dfandc  811  dfordc  824  dfor2dc  827  pm4.79dc  842  orimdidc  845  pm5.54dc  860  pm5.62dc  886  bimsc1  904  modc  1984  euan  1997  exmoeudc  2004  nebidc  2325  cgsexg  2634  cgsex2g  2635  cgsex4g  2636  elab3gf  2743  abidnf  2760  elsn2g  3427  difsn  3523  prel12  3563  dfnfc2  3619  intmin4  3664  dfiin2g  3711  elpw2g  3931  ordsucg  4246  ssrel  4446  ssrel2  4448  ssrelrel  4458  releldmb  4589  relelrnb  4590  cnveqb  4796  dmsnopg  4812  relcnvtr  4860  relcnvexb  4877  f1ocnvb  5160  ffvresb  5349  fconstfvm  5400  fnoprabg  5622  dfsmo2  5925  nntri2  6096  nntri1  6097  en1bg  6303  nngt1ne1  8073  znegclb  8384  iccneg  9011  fzsn  9084  fz1sbc  9113  fzofzp1b  9237  ceilqidz  9318  flqeqceilz  9320  reim0b  9749  rexanre  10106  dvdsext  10255  zob  10291  bj-om  10732