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  908  pm5.63dc  946  pm4.83dc  951  pm5.71dc  961  19.33b2  1629  19.9t  1642  sb4b  1834  a16gb  1865  euor2  2084  eupickbi  2108  ceqsalg  2767  eqvincg  2863  ddifstab  3269  csbprc  3470  undif4  3487  eqifdc  3571  sssnm  3756  sneqbg  3765  opthpr  3774  elpwuni  3978  ss1o0el1  4199  exmid01  4200  exmidundif  4208  eusv2i  4457  reusv3  4462  iunpw  4482  suc11g  4558  ssxpbm  5066  ssxp1  5067  ssxp2  5068  xp11m  5069  2elresin  5329  mpteqb  5608  f1fveq  5775  f1elima  5776  f1imass  5777  fliftf  5802  nnsucuniel  6498  iserd  6563  ecopovtrn  6634  ecopover  6635  ecopovtrng  6637  ecopoverg  6638  map0g  6690  fopwdom  6838  f1finf1o  6948  mkvprop  7158  addcanpig  7335  mulcanpig  7336  srpospr  7784  readdcan  8099  cnegexlem1  8134  addcan  8139  addcan2  8140  neg11  8210  negreb  8224  add20  8433  cru  8561  mulcanapd  8620  uz11  9552  eqreznegel  9616  lbzbi  9618  xneg11  9836  xnn0xadd0  9869  xsubge0  9883  elioc2  9938  elico2  9939  elicc2  9940  fzopth  10063  2ffzeq  10143  flqidz  10288  addmodlteq  10400  frec2uzrand  10407  expcan  10698  nn0opthd  10704  fz1eqb  10772  cj11  10916  sqrt0  11015  recan  11120  0dvds  11820  dvds1  11861  alzdvds  11862  nn0enne  11909  nn0oddm1d2  11916  nnoddm1d2  11917  divalgmod  11934  gcdeq0  11980  algcvgblem  12051  prmexpb  12153  ennnfonelemim  12427  grprcan  12915  grplcan  12937  grpinv11  12944  tgdom  13611  en1top  13616  hmeocnvb  13857  metrest  14045  lgsne0  14478  2lgsoddprmlem3  14498  bj-nnbist  14535  bj-nnbidc  14548  bj-peano4  14746  bj-nn0sucALT  14769