Theorem impbid1 141

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1	⊢ (𝜑 → (𝜓 → 𝜒))
impbid1.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
impbid1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impbid1.2	. . 3 ⊢ (𝜒 → 𝜓)
3	2	a1i 9	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	impbid 128	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  iba  298  ibar  299  pm4.81dc  893  pm5.63dc  930  pm4.83dc  935  pm5.71dc  945  19.33b2  1608  19.9t  1621  sb4b  1806  a16gb  1837  euor2  2057  eupickbi  2081  ceqsalg  2714  eqvincg  2809  ddifstab  3208  csbprc  3408  undif4  3425  eqifdc  3506  sssnm  3681  sneqbg  3690  opthpr  3699  elpwuni  3902  exmid01  4121  exmidundif  4129  eusv2i  4376  reusv3  4381  iunpw  4401  suc11g  4472  ssxpbm  4974  ssxp1  4975  ssxp2  4976  xp11m  4977  2elresin  5234  mpteqb  5511  f1fveq  5673  f1elima  5674  f1imass  5675  fliftf  5700  nnsucuniel  6391  iserd  6455  ecopovtrn  6526  ecopover  6527  ecopovtrng  6529  ecopoverg  6530  map0g  6582  fopwdom  6730  f1finf1o  6835  mkvprop  7032  addcanpig  7142  mulcanpig  7143  srpospr  7591  readdcan  7902  cnegexlem1  7937  addcan  7942  addcan2  7943  neg11  8013  negreb  8027  add20  8236  cru  8364  mulcanapd  8422  uz11  9348  eqreznegel  9406  lbzbi  9408  xneg11  9617  xnn0xadd0  9650  xsubge0  9664  elioc2  9719  elico2  9720  elicc2  9721  fzopth  9841  2ffzeq  9918  flqidz  10059  addmodlteq  10171  frec2uzrand  10178  expcan  10463  nn0opthd  10468  fz1eqb  10537  cj11  10677  sqrt0  10776  recan  10881  0dvds  11513  dvds1  11551  alzdvds  11552  nn0enne  11599  nn0oddm1d2  11606  nnoddm1d2  11607  divalgmod  11624  gcdeq0  11665  algcvgblem  11730  prmexpb  11829  ennnfonelemim  11937  tgdom  12241  en1top  12246  hmeocnvb  12487  metrest  12675  bj-nnbist  12953  bj-nnbidc  12962  bj-peano4  13153  bj-nn0sucALT  13176