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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  impbid2  143  iba  300  ibar  301  pm4.81dc  920  pm5.63dc  959  pm4.83dc  964  pm5.71dc  974  19.33b2  1682  19.9t  1695  sb4b  1887  a16gb  1918  euor2  2145  eupickbi  2169  ceqsalg  2850  eqvincg  2950  ddifstab  3361  csbprc  3572  undif4  3587  eqifdc  3677  ifnebibdc  3686  ssprsseq  3877  sssnm  3879  sneqbg  3888  opthpr  3897  elpwuni  4102  ss1o0el1  4334  exmid01  4335  exmidundif  4343  eusv2i  4601  reusv3  4606  iunpw  4626  suc11g  4704  reldmm  5000  ssxpbm  5223  ssxp1  5224  ssxp2  5225  xp11m  5226  2elresin  5494  mpteqb  5796  f1fveq  5978  f1elima  5979  f1imass  5980  fliftf  6005  nnsucuniel  6768  iserd  6833  ecopovtrn  6906  ecopover  6907  ecopovtrng  6909  ecopoverg  6910  mapfset  6945  map0g  6969  fopwdom  7136  f1finf1o  7264  mkvprop  7498  addcanpig  7701  mulcanpig  7702  srpospr  8150  readdcan  8467  cnegexlem1  8502  addcan  8507  addcan2  8508  neg11  8578  negreb  8592  add20  8803  cru  8932  mulcanapd  8991  uz11  9954  eqreznegel  10023  lbzbi  10025  xneg11  10246  xnn0xadd0  10279  xsubge0  10293  elioc2  10348  elico2  10349  elicc2  10350  fzopth  10477  2ffzeq  10558  flqidz  10734  addmodlteq  10848  frec2uzrand  10855  nninfinf  10893  resq01  11108  expcan  11168  nn0opthd  11174  fz1eqb  11243  wrdnval  11349  eqwrd  11359  ccatalpha  11395  wrdl1s1  11412  ccatopth  11502  ccatopth2  11503  sq01  11674  cj11  11685  sqrt0  11784  recan  11890  0dvds  12594  dvds1  12636  alzdvds  12637  nn0enne  12685  nn0oddm1d2  12692  nnoddm1d2  12693  divalgmod  12710  gcdeq0  12770  algcvgblem  12843  prmexpb  12946  4sqexercise2  13198  4sqlemsdc  13199  4sqlem11  13200  ennnfonelemim  13364  grprcan  13891  grplcan  13916  grpinv11  13923  isnzr2  14540  znidomb  15042  tgdom  15222  en1top  15227  hmeocnvb  15468  metrest  15656  pellexlem3  16150  perfect  16199  lgsne0  16255  2lgs  16321  2lgsoddprmlem3  16328  wrdupgren  16435  wrdumgren  16445  usgrausgrben  16511  upgriswlkdc  16699  bj-nnbist  16870  bj-nnbidc  16883  bj-peano4  17079  bj-nn0sucALT  17102