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  915  pm5.63dc  954  pm4.83dc  959  pm5.71dc  969  19.33b2  1677  19.9t  1690  sb4b  1882  a16gb  1913  euor2  2138  eupickbi  2162  ceqsalg  2831  eqvincg  2930  ddifstab  3339  csbprc  3540  undif4  3557  eqifdc  3642  ifnebibdc  3651  ssprsseq  3835  sssnm  3837  sneqbg  3846  opthpr  3855  elpwuni  4060  ss1o0el1  4287  exmid01  4288  exmidundif  4296  eusv2i  4552  reusv3  4557  iunpw  4577  suc11g  4655  reldmm  4950  ssxpbm  5172  ssxp1  5173  ssxp2  5174  xp11m  5175  2elresin  5443  mpteqb  5737  f1fveq  5912  f1elima  5913  f1imass  5914  fliftf  5939  nnsucuniel  6662  iserd  6727  ecopovtrn  6800  ecopover  6801  ecopovtrng  6803  ecopoverg  6804  map0g  6856  fopwdom  7021  f1finf1o  7145  mkvprop  7356  addcanpig  7553  mulcanpig  7554  srpospr  8002  readdcan  8318  cnegexlem1  8353  addcan  8358  addcan2  8359  neg11  8429  negreb  8443  add20  8653  cru  8781  mulcanapd  8840  uz11  9778  eqreznegel  9847  lbzbi  9849  xneg11  10068  xnn0xadd0  10101  xsubge0  10115  elioc2  10170  elico2  10171  elicc2  10172  fzopth  10295  2ffzeq  10375  flqidz  10545  addmodlteq  10659  frec2uzrand  10666  nninfinf  10704  expcan  10977  nn0opthd  10983  fz1eqb  11051  wrdnval  11143  eqwrd  11153  ccatalpha  11189  wrdl1s1  11206  ccatopth  11296  ccatopth2  11297  cj11  11465  sqrt0  11564  recan  11669  0dvds  12371  dvds1  12413  alzdvds  12414  nn0enne  12462  nn0oddm1d2  12469  nnoddm1d2  12470  divalgmod  12487  gcdeq0  12547  algcvgblem  12620  prmexpb  12722  4sqexercise2  12971  4sqlemsdc  12972  4sqlem11  12973  ennnfonelemim  13044  grprcan  13619  grplcan  13644  grpinv11  13651  isnzr2  14197  znidomb  14671  tgdom  14795  en1top  14800  hmeocnvb  15041  metrest  15229  perfect  15724  lgsne0  15766  2lgs  15832  2lgsoddprmlem3  15839  wrdupgren  15946  wrdumgren  15956  usgrausgrben  16022  upgriswlkdc  16210  bj-nnbist  16340  bj-nnbidc  16353  bj-peano4  16550  bj-nn0sucALT  16573