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  3830  sssnm  3832  sneqbg  3841  opthpr  3850  elpwuni  4055  ss1o0el1  4281  exmid01  4282  exmidundif  4290  eusv2i  4546  reusv3  4551  iunpw  4571  suc11g  4649  reldmm  4942  ssxpbm  5164  ssxp1  5165  ssxp2  5166  xp11m  5167  2elresin  5434  mpteqb  5727  f1fveq  5902  f1elima  5903  f1imass  5904  fliftf  5929  nnsucuniel  6649  iserd  6714  ecopovtrn  6787  ecopover  6788  ecopovtrng  6790  ecopoverg  6791  map0g  6843  fopwdom  7005  f1finf1o  7125  mkvprop  7336  addcanpig  7532  mulcanpig  7533  srpospr  7981  readdcan  8297  cnegexlem1  8332  addcan  8337  addcan2  8338  neg11  8408  negreb  8422  add20  8632  cru  8760  mulcanapd  8819  uz11  9757  eqreznegel  9821  lbzbi  9823  xneg11  10042  xnn0xadd0  10075  xsubge0  10089  elioc2  10144  elico2  10145  elicc2  10146  fzopth  10269  2ffzeq  10349  flqidz  10518  addmodlteq  10632  frec2uzrand  10639  nninfinf  10677  expcan  10950  nn0opthd  10956  fz1eqb  11024  wrdnval  11115  eqwrd  11125  ccatalpha  11161  wrdl1s1  11178  ccatopth  11263  ccatopth2  11264  cj11  11431  sqrt0  11530  recan  11635  0dvds  12337  dvds1  12379  alzdvds  12380  nn0enne  12428  nn0oddm1d2  12435  nnoddm1d2  12436  divalgmod  12453  gcdeq0  12513  algcvgblem  12586  prmexpb  12688  4sqexercise2  12937  4sqlemsdc  12938  4sqlem11  12939  ennnfonelemim  13010  grprcan  13585  grplcan  13610  grpinv11  13617  isnzr2  14163  znidomb  14637  tgdom  14761  en1top  14766  hmeocnvb  15007  metrest  15195  perfect  15690  lgsne0  15732  2lgs  15798  2lgsoddprmlem3  15805  wrdupgren  15911  wrdumgren  15921  usgrausgrben  15985  upgriswlkdc  16101  bj-nnbist  16163  bj-nnbidc  16176  bj-peano4  16373  bj-nn0sucALT  16396