Theorem impbid1 141

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 128	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  iba  298  ibar  299  pm4.81dc  894  pm5.63dc  931  pm4.83dc  936  pm5.71dc  946  19.33b2  1609  19.9t  1622  sb4b  1814  a16gb  1845  euor2  2064  eupickbi  2088  ceqsalg  2740  eqvincg  2836  ddifstab  3239  csbprc  3439  undif4  3456  eqifdc  3539  sssnm  3717  sneqbg  3726  opthpr  3735  elpwuni  3938  ss1o0el1  4158  exmid01  4159  exmidundif  4167  eusv2i  4414  reusv3  4419  iunpw  4439  suc11g  4515  ssxpbm  5020  ssxp1  5021  ssxp2  5022  xp11m  5023  2elresin  5280  mpteqb  5557  f1fveq  5719  f1elima  5720  f1imass  5721  fliftf  5746  nnsucuniel  6439  iserd  6503  ecopovtrn  6574  ecopover  6575  ecopovtrng  6577  ecopoverg  6578  map0g  6630  fopwdom  6778  f1finf1o  6888  mkvprop  7095  addcanpig  7248  mulcanpig  7249  srpospr  7697  readdcan  8009  cnegexlem1  8044  addcan  8049  addcan2  8050  neg11  8120  negreb  8134  add20  8343  cru  8471  mulcanapd  8529  uz11  9455  eqreznegel  9516  lbzbi  9518  xneg11  9731  xnn0xadd0  9764  xsubge0  9778  elioc2  9833  elico2  9834  elicc2  9835  fzopth  9956  2ffzeq  10033  flqidz  10178  addmodlteq  10290  frec2uzrand  10297  expcan  10583  nn0opthd  10589  fz1eqb  10658  cj11  10798  sqrt0  10897  recan  11002  0dvds  11699  dvds1  11737  alzdvds  11738  nn0enne  11785  nn0oddm1d2  11792  nnoddm1d2  11793  divalgmod  11810  gcdeq0  11852  algcvgblem  11917  prmexpb  12016  ennnfonelemim  12136  tgdom  12443  en1top  12448  hmeocnvb  12689  metrest  12877  bj-nnbist  13289  bj-nnbidc  13300  bj-peano4  13501  bj-nn0sucALT  13524