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  687  biorf  746  biorfi  748  pm4.72  829  con34bdc  873  notnotbdc  874  dfandc  886  imanst  890  dfordc  894  dfor2dc  897  pm4.79dc  905  orimdidc  908  pm5.54dc  920  pm5.62dc  948  bimsc1  966  modc  2097  euan  2110  exmoeudc  2117  nebidc  2456  cgsexg  2807  cgsex2g  2808  cgsex4g  2809  elab3gf  2923  abidnf  2941  elsn2g  3666  difsn  3770  prel12  3812  dfnfc2  3868  intmin4  3913  dfiin2g  3960  elpw2g  4200  ordsucg  4550  ssrel  4763  ssrel2  4765  ssrelrel  4775  releldmb  4915  relelrnb  4916  cnveqb  5138  dmsnopg  5154  relcnvtr  5202  relcnvexb  5222  f1ocnvb  5536  ffvresb  5743  fconstfvm  5802  fnoprabg  6046  dfsmo2  6373  nntri2  6580  nntri1  6582  en1bg  6892  pw2f1odclem  6931  fieq0  7078  djulclb  7157  ismkvnex  7257  nngt1ne1  9071  znegclb  9405  iccneg  10111  fzsn  10188  fz1sbc  10218  fzofzp1b  10357  ceilqidz  10461  flqeqceilz  10463  reim0b  11173  rexanre  11531  dvdsext  12166  zob  12202  pc11  12654  pcz  12655  gsumval2  13229  issubg2m  13525  issubg4m  13529  ghmmhmb  13590  opprrngbg  13840  opprringbg  13842  issubrng2  13972  issubrg2  14003  eltg3  14529  bastop  14547  cnptoprest  14711  cos11  15325  zabsle1  15476  lgsabs1  15516  lgsquadlem2  15555  bj-om  15873