Theorem impbid1 142

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 129	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  impbid2  143  iba  300  ibar  301  pm4.81dc  909  pm5.63dc  948  pm4.83dc  953  pm5.71dc  963  19.33b2  1643  19.9t  1656  sb4b  1848  a16gb  1879  euor2  2103  eupickbi  2127  ceqsalg  2791  eqvincg  2888  ddifstab  3296  csbprc  3497  undif4  3514  eqifdc  3597  ifnebibdc  3605  sssnm  3785  sneqbg  3794  opthpr  3803  elpwuni  4007  ss1o0el1  4231  exmid01  4232  exmidundif  4240  eusv2i  4491  reusv3  4496  iunpw  4516  suc11g  4594  ssxpbm  5106  ssxp1  5107  ssxp2  5108  xp11m  5109  2elresin  5370  mpteqb  5653  f1fveq  5820  f1elima  5821  f1imass  5822  fliftf  5847  nnsucuniel  6554  iserd  6619  ecopovtrn  6692  ecopover  6693  ecopovtrng  6695  ecopoverg  6696  map0g  6748  fopwdom  6898  f1finf1o  7014  mkvprop  7225  addcanpig  7403  mulcanpig  7404  srpospr  7852  readdcan  8168  cnegexlem1  8203  addcan  8208  addcan2  8209  neg11  8279  negreb  8293  add20  8503  cru  8631  mulcanapd  8690  uz11  9626  eqreznegel  9690  lbzbi  9692  xneg11  9911  xnn0xadd0  9944  xsubge0  9958  elioc2  10013  elico2  10014  elicc2  10015  fzopth  10138  2ffzeq  10218  flqidz  10378  addmodlteq  10492  frec2uzrand  10499  nninfinf  10537  expcan  10810  nn0opthd  10816  fz1eqb  10884  wrdnval  10967  eqwrd  10977  cj11  11072  sqrt0  11171  recan  11276  0dvds  11978  dvds1  12020  alzdvds  12021  nn0enne  12069  nn0oddm1d2  12076  nnoddm1d2  12077  divalgmod  12094  gcdeq0  12154  algcvgblem  12227  prmexpb  12329  4sqexercise2  12578  4sqlemsdc  12579  4sqlem11  12580  ennnfonelemim  12651  grprcan  13179  grplcan  13204  grpinv11  13211  isnzr2  13750  znidomb  14224  tgdom  14318  en1top  14323  hmeocnvb  14564  metrest  14752  perfect  15247  lgsne0  15289  2lgs  15355  2lgsoddprmlem3  15362  bj-nnbist  15400  bj-nnbidc  15413  bj-peano4  15611  bj-nn0sucALT  15634