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  913  pm5.63dc  952  pm4.83dc  957  pm5.71dc  967  19.33b2  1675  19.9t  1688  sb4b  1880  a16gb  1911  euor2  2136  eupickbi  2160  ceqsalg  2828  eqvincg  2927  ddifstab  3336  csbprc  3537  undif4  3554  eqifdc  3639  ifnebibdc  3648  ssprsseq  3829  sssnm  3831  sneqbg  3840  opthpr  3849  elpwuni  4054  ss1o0el1  4280  exmid01  4281  exmidundif  4289  eusv2i  4545  reusv3  4550  iunpw  4570  suc11g  4648  reldmm  4941  ssxpbm  5163  ssxp1  5164  ssxp2  5165  xp11m  5166  2elresin  5433  mpteqb  5724  f1fveq  5895  f1elima  5896  f1imass  5897  fliftf  5922  nnsucuniel  6639  iserd  6704  ecopovtrn  6777  ecopover  6778  ecopovtrng  6780  ecopoverg  6781  map0g  6833  fopwdom  6993  f1finf1o  7110  mkvprop  7321  addcanpig  7517  mulcanpig  7518  srpospr  7966  readdcan  8282  cnegexlem1  8317  addcan  8322  addcan2  8323  neg11  8393  negreb  8407  add20  8617  cru  8745  mulcanapd  8804  uz11  9741  eqreznegel  9805  lbzbi  9807  xneg11  10026  xnn0xadd0  10059  xsubge0  10073  elioc2  10128  elico2  10129  elicc2  10130  fzopth  10253  2ffzeq  10333  flqidz  10501  addmodlteq  10615  frec2uzrand  10622  nninfinf  10660  expcan  10933  nn0opthd  10939  fz1eqb  11007  wrdnval  11097  eqwrd  11107  wrdl1s1  11158  ccatopth  11243  ccatopth2  11244  cj11  11411  sqrt0  11510  recan  11615  0dvds  12317  dvds1  12359  alzdvds  12360  nn0enne  12408  nn0oddm1d2  12415  nnoddm1d2  12416  divalgmod  12433  gcdeq0  12493  algcvgblem  12566  prmexpb  12668  4sqexercise2  12917  4sqlemsdc  12918  4sqlem11  12919  ennnfonelemim  12990  grprcan  13565  grplcan  13590  grpinv11  13597  isnzr2  14142  znidomb  14616  tgdom  14740  en1top  14745  hmeocnvb  14986  metrest  15174  perfect  15669  lgsne0  15711  2lgs  15777  2lgsoddprmlem3  15784  wrdupgren  15890  wrdumgren  15900  usgrausgrben  15964  bj-nnbist  16066  bj-nnbidc  16079  bj-peano4  16276  bj-nn0sucALT  16299