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  908  pm5.63dc  946  pm4.83dc  951  pm5.71dc  961  19.33b2  1629  19.9t  1642  sb4b  1834  a16gb  1865  euor2  2084  eupickbi  2108  ceqsalg  2765  eqvincg  2861  ddifstab  3267  csbprc  3468  undif4  3485  eqifdc  3569  sssnm  3754  sneqbg  3763  opthpr  3772  elpwuni  3975  ss1o0el1  4196  exmid01  4197  exmidundif  4205  eusv2i  4454  reusv3  4459  iunpw  4479  suc11g  4555  ssxpbm  5063  ssxp1  5064  ssxp2  5065  xp11m  5066  2elresin  5326  mpteqb  5605  f1fveq  5770  f1elima  5771  f1imass  5772  fliftf  5797  nnsucuniel  6493  iserd  6558  ecopovtrn  6629  ecopover  6630  ecopovtrng  6632  ecopoverg  6633  map0g  6685  fopwdom  6833  f1finf1o  6943  mkvprop  7153  addcanpig  7330  mulcanpig  7331  srpospr  7779  readdcan  8093  cnegexlem1  8128  addcan  8133  addcan2  8134  neg11  8204  negreb  8218  add20  8427  cru  8555  mulcanapd  8614  uz11  9546  eqreznegel  9610  lbzbi  9612  xneg11  9830  xnn0xadd0  9863  xsubge0  9877  elioc2  9932  elico2  9933  elicc2  9934  fzopth  10056  2ffzeq  10136  flqidz  10281  addmodlteq  10393  frec2uzrand  10400  expcan  10689  nn0opthd  10695  fz1eqb  10763  cj11  10907  sqrt0  11006  recan  11111  0dvds  11811  dvds1  11851  alzdvds  11852  nn0enne  11899  nn0oddm1d2  11906  nnoddm1d2  11907  divalgmod  11924  gcdeq0  11970  algcvgblem  12041  prmexpb  12143  ennnfonelemim  12417  grprcan  12842  grplcan  12864  grpinv11  12871  tgdom  13443  en1top  13448  hmeocnvb  13689  metrest  13877  lgsne0  14310  bj-nnbist  14356  bj-nnbidc  14369  bj-peano4  14567  bj-nn0sucALT  14590