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  7499  addcanpig  7702  mulcanpig  7703  srpospr  8151  readdcan  8468  cnegexlem1  8503  addcan  8508  addcan2  8509  neg11  8579  negreb  8593  add20  8804  cru  8933  mulcanapd  8992  uz11  9955  eqreznegel  10024  lbzbi  10026  xneg11  10247  xnn0xadd0  10280  xsubge0  10294  elioc2  10349  elico2  10350  elicc2  10351  fzopth  10478  2ffzeq  10559  flqidz  10736  addmodlteq  10850  frec2uzrand  10857  nninfinf  10895  resq01  11110  expcan  11170  nn0opthd  11176  fz1eqb  11245  wrdnval  11351  eqwrd  11361  ccatalpha  11397  wrdl1s1  11414  ccatopth  11504  ccatopth2  11505  sq01  11676  cj11  11687  sqrt0  11786  recan  11892  0dvds  12597  dvds1  12639  alzdvds  12640  nn0enne  12688  nn0oddm1d2  12695  nnoddm1d2  12696  divalgmod  12713  gcdeq0  12773  algcvgblem  12846  prmexpb  12949  4sqexercise2  13201  4sqlemsdc  13202  4sqlem11  13203  ennnfonelemim  13367  grprcan  13895  grplcan  13920  grpinv11  13927  isnzr2  14575  znidomb  15077  tgdom  15264  en1top  15269  hmeocnvb  15510  metrest  15698  pellexlem3  16192  perfect  16262  lgsne0  16323  2lgs  16389  2lgsoddprmlem3  16396  wrdupgren  16503  wrdumgren  16513  usgrausgrben  16579  upgriswlkdc  16767  bj-nnbist  16938  bj-nnbidc  16951  bj-peano4  17147  bj-nn0sucALT  17170