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  5913  f1elima  5914  f1imass  5915  fliftf  5940  nnsucuniel  6663  iserd  6728  ecopovtrn  6801  ecopover  6802  ecopovtrng  6804  ecopoverg  6805  map0g  6857  fopwdom  7022  f1finf1o  7146  mkvprop  7357  addcanpig  7554  mulcanpig  7555  srpospr  8003  readdcan  8319  cnegexlem1  8354  addcan  8359  addcan2  8360  neg11  8430  negreb  8444  add20  8654  cru  8782  mulcanapd  8841  uz11  9779  eqreznegel  9848  lbzbi  9850  xneg11  10069  xnn0xadd0  10102  xsubge0  10116  elioc2  10171  elico2  10172  elicc2  10173  fzopth  10296  2ffzeq  10376  flqidz  10547  addmodlteq  10661  frec2uzrand  10668  nninfinf  10706  expcan  10979  nn0opthd  10985  fz1eqb  11053  wrdnval  11148  eqwrd  11158  ccatalpha  11194  wrdl1s1  11211  ccatopth  11301  ccatopth2  11302  cj11  11483  sqrt0  11582  recan  11687  0dvds  12390  dvds1  12432  alzdvds  12433  nn0enne  12481  nn0oddm1d2  12488  nnoddm1d2  12489  divalgmod  12506  gcdeq0  12566  algcvgblem  12639  prmexpb  12741  4sqexercise2  12990  4sqlemsdc  12991  4sqlem11  12992  ennnfonelemim  13063  grprcan  13638  grplcan  13663  grpinv11  13670  isnzr2  14217  znidomb  14691  tgdom  14815  en1top  14820  hmeocnvb  15061  metrest  15249  perfect  15744  lgsne0  15786  2lgs  15852  2lgsoddprmlem3  15859  wrdupgren  15966  wrdumgren  15976  usgrausgrben  16042  upgriswlkdc  16230  bj-nnbist  16391  bj-nnbidc  16404  bj-peano4  16601  bj-nn0sucALT  16624