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  909  pm5.63dc  948  pm4.83dc  953  pm5.71dc  963  19.33b2  1643  19.9t  1656  sb4b  1848  a16gb  1879  euor2  2103  eupickbi  2127  ceqsalg  2791  eqvincg  2888  ddifstab  3296  csbprc  3497  undif4  3514  eqifdc  3597  ifnebibdc  3605  sssnm  3785  sneqbg  3794  opthpr  3803  elpwuni  4007  ss1o0el1  4231  exmid01  4232  exmidundif  4240  eusv2i  4491  reusv3  4496  iunpw  4516  suc11g  4594  ssxpbm  5106  ssxp1  5107  ssxp2  5108  xp11m  5109  2elresin  5372  mpteqb  5655  f1fveq  5822  f1elima  5823  f1imass  5824  fliftf  5849  nnsucuniel  6562  iserd  6627  ecopovtrn  6700  ecopover  6701  ecopovtrng  6703  ecopoverg  6704  map0g  6756  fopwdom  6906  f1finf1o  7022  mkvprop  7233  addcanpig  7420  mulcanpig  7421  srpospr  7869  readdcan  8185  cnegexlem1  8220  addcan  8225  addcan2  8226  neg11  8296  negreb  8310  add20  8520  cru  8648  mulcanapd  8707  uz11  9643  eqreznegel  9707  lbzbi  9709  xneg11  9928  xnn0xadd0  9961  xsubge0  9975  elioc2  10030  elico2  10031  elicc2  10032  fzopth  10155  2ffzeq  10235  flqidz  10395  addmodlteq  10509  frec2uzrand  10516  nninfinf  10554  expcan  10827  nn0opthd  10833  fz1eqb  10901  wrdnval  10984  eqwrd  10994  cj11  11089  sqrt0  11188  recan  11293  0dvds  11995  dvds1  12037  alzdvds  12038  nn0enne  12086  nn0oddm1d2  12093  nnoddm1d2  12094  divalgmod  12111  gcdeq0  12171  algcvgblem  12244  prmexpb  12346  4sqexercise2  12595  4sqlemsdc  12596  4sqlem11  12597  ennnfonelemim  12668  grprcan  13241  grplcan  13266  grpinv11  13273  isnzr2  13818  znidomb  14292  tgdom  14416  en1top  14421  hmeocnvb  14662  metrest  14850  perfect  15345  lgsne0  15387  2lgs  15453  2lgsoddprmlem3  15460  bj-nnbist  15498  bj-nnbidc  15511  bj-peano4  15709  bj-nn0sucALT  15732