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  1651  19.9t  1664  sb4b  1856  a16gb  1887  euor2  2111  eupickbi  2135  ceqsalg  2799  eqvincg  2896  ddifstab  3304  csbprc  3505  undif4  3522  eqifdc  3606  ifnebibdc  3614  sssnm  3794  sneqbg  3803  opthpr  3812  elpwuni  4016  ss1o0el1  4240  exmid01  4241  exmidundif  4249  eusv2i  4501  reusv3  4506  iunpw  4526  suc11g  4604  ssxpbm  5117  ssxp1  5118  ssxp2  5119  xp11m  5120  2elresin  5386  mpteqb  5669  f1fveq  5840  f1elima  5841  f1imass  5842  fliftf  5867  nnsucuniel  6580  iserd  6645  ecopovtrn  6718  ecopover  6719  ecopovtrng  6721  ecopoverg  6722  map0g  6774  fopwdom  6932  f1finf1o  7048  mkvprop  7259  addcanpig  7446  mulcanpig  7447  srpospr  7895  readdcan  8211  cnegexlem1  8246  addcan  8251  addcan2  8252  neg11  8322  negreb  8336  add20  8546  cru  8674  mulcanapd  8733  uz11  9670  eqreznegel  9734  lbzbi  9736  xneg11  9955  xnn0xadd0  9988  xsubge0  10002  elioc2  10057  elico2  10058  elicc2  10059  fzopth  10182  2ffzeq  10262  flqidz  10427  addmodlteq  10541  frec2uzrand  10548  nninfinf  10586  expcan  10859  nn0opthd  10865  fz1eqb  10933  wrdnval  11022  eqwrd  11032  wrdl1s1  11082  cj11  11187  sqrt0  11286  recan  11391  0dvds  12093  dvds1  12135  alzdvds  12136  nn0enne  12184  nn0oddm1d2  12191  nnoddm1d2  12192  divalgmod  12209  gcdeq0  12269  algcvgblem  12342  prmexpb  12444  4sqexercise2  12693  4sqlemsdc  12694  4sqlem11  12695  ennnfonelemim  12766  grprcan  13340  grplcan  13365  grpinv11  13372  isnzr2  13917  znidomb  14391  tgdom  14515  en1top  14520  hmeocnvb  14761  metrest  14949  perfect  15444  lgsne0  15486  2lgs  15552  2lgsoddprmlem3  15559  bj-nnbist  15642  bj-nnbidc  15655  bj-peano4  15853  bj-nn0sucALT  15876