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-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  iba  296  ibar  297  pm4.81dc  876  pm5.63dc  913  pm4.83dc  918  pm5.71dc  928  19.33b2  1591  19.9t  1604  sb4b  1788  a16gb  1819  euor2  2033  eupickbi  2057  ceqsalg  2685  eqvincg  2779  ddifstab  3174  csbprc  3374  undif4  3391  eqifdc  3472  sssnm  3647  sneqbg  3656  opthpr  3665  elpwuni  3868  exmid01  4081  exmidundif  4089  eusv2i  4336  reusv3  4341  iunpw  4361  suc11g  4432  ssxpbm  4932  ssxp1  4933  ssxp2  4934  xp11m  4935  2elresin  5192  mpteqb  5465  f1fveq  5627  f1elima  5628  f1imass  5629  fliftf  5654  nnsucuniel  6345  iserd  6409  ecopovtrn  6480  ecopover  6481  ecopovtrng  6483  ecopoverg  6484  map0g  6536  fopwdom  6683  f1finf1o  6787  mkvprop  6982  addcanpig  7090  mulcanpig  7091  srpospr  7525  readdcan  7825  cnegexlem1  7860  addcan  7865  addcan2  7866  neg11  7936  negreb  7950  add20  8155  cru  8282  mulcanapd  8335  uz11  9250  eqreznegel  9308  lbzbi  9310  xneg11  9510  xnn0xadd0  9543  xsubge0  9557  elioc2  9612  elico2  9613  elicc2  9614  fzopth  9734  2ffzeq  9811  flqidz  9952  addmodlteq  10064  frec2uzrand  10071  expcan  10356  nn0opthd  10361  fz1eqb  10430  cj11  10570  sqrt0  10668  recan  10773  0dvds  11361  dvds1  11399  alzdvds  11400  nn0enne  11447  nn0oddm1d2  11454  nnoddm1d2  11455  divalgmod  11472  gcdeq0  11513  algcvgblem  11576  prmexpb  11675  ennnfonelemim  11782  tgdom  12084  en1top  12089  metrest  12495  bj-nnbist  12646  bj-nnbidc  12655  bj-peano4  12845  bj-nn0sucALT  12868