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  2829  eqvincg  2928  ddifstab  3337  csbprc  3538  undif4  3555  eqifdc  3640  ifnebibdc  3649  ssprsseq  3833  sssnm  3835  sneqbg  3844  opthpr  3853  elpwuni  4058  ss1o0el1  4285  exmid01  4286  exmidundif  4294  eusv2i  4550  reusv3  4555  iunpw  4575  suc11g  4653  reldmm  4948  ssxpbm  5170  ssxp1  5171  ssxp2  5172  xp11m  5173  2elresin  5440  mpteqb  5733  f1fveq  5908  f1elima  5909  f1imass  5910  fliftf  5935  nnsucuniel  6658  iserd  6723  ecopovtrn  6796  ecopover  6797  ecopovtrng  6799  ecopoverg  6800  map0g  6852  fopwdom  7017  f1finf1o  7137  mkvprop  7348  addcanpig  7544  mulcanpig  7545  srpospr  7993  readdcan  8309  cnegexlem1  8344  addcan  8349  addcan2  8350  neg11  8420  negreb  8434  add20  8644  cru  8772  mulcanapd  8831  uz11  9769  eqreznegel  9838  lbzbi  9840  xneg11  10059  xnn0xadd0  10092  xsubge0  10106  elioc2  10161  elico2  10162  elicc2  10163  fzopth  10286  2ffzeq  10366  flqidz  10536  addmodlteq  10650  frec2uzrand  10657  nninfinf  10695  expcan  10968  nn0opthd  10974  fz1eqb  11042  wrdnval  11134  eqwrd  11144  ccatalpha  11180  wrdl1s1  11197  ccatopth  11287  ccatopth2  11288  cj11  11456  sqrt0  11555  recan  11660  0dvds  12362  dvds1  12404  alzdvds  12405  nn0enne  12453  nn0oddm1d2  12460  nnoddm1d2  12461  divalgmod  12478  gcdeq0  12538  algcvgblem  12611  prmexpb  12713  4sqexercise2  12962  4sqlemsdc  12963  4sqlem11  12964  ennnfonelemim  13035  grprcan  13610  grplcan  13635  grpinv11  13642  isnzr2  14188  znidomb  14662  tgdom  14786  en1top  14791  hmeocnvb  15032  metrest  15220  perfect  15715  lgsne0  15757  2lgs  15823  2lgsoddprmlem3  15830  wrdupgren  15937  wrdumgren  15947  usgrausgrben  16011  upgriswlkdc  16157  bj-nnbist  16276  bj-nnbidc  16289  bj-peano4  16486  bj-nn0sucALT  16509