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  910  pm5.63dc  949  pm4.83dc  954  pm5.71dc  964  19.33b2  1653  19.9t  1666  sb4b  1858  a16gb  1889  euor2  2114  eupickbi  2138  ceqsalg  2805  eqvincg  2904  ddifstab  3313  csbprc  3514  undif4  3531  eqifdc  3616  ifnebibdc  3625  ssprsseq  3806  sssnm  3808  sneqbg  3817  opthpr  3826  elpwuni  4031  ss1o0el1  4257  exmid01  4258  exmidundif  4266  eusv2i  4520  reusv3  4525  iunpw  4545  suc11g  4623  ssxpbm  5137  ssxp1  5138  ssxp2  5139  xp11m  5140  2elresin  5406  mpteqb  5693  f1fveq  5864  f1elima  5865  f1imass  5866  fliftf  5891  nnsucuniel  6604  iserd  6669  ecopovtrn  6742  ecopover  6743  ecopovtrng  6745  ecopoverg  6746  map0g  6798  fopwdom  6958  f1finf1o  7075  mkvprop  7286  addcanpig  7482  mulcanpig  7483  srpospr  7931  readdcan  8247  cnegexlem1  8282  addcan  8287  addcan2  8288  neg11  8358  negreb  8372  add20  8582  cru  8710  mulcanapd  8769  uz11  9706  eqreznegel  9770  lbzbi  9772  xneg11  9991  xnn0xadd0  10024  xsubge0  10038  elioc2  10093  elico2  10094  elicc2  10095  fzopth  10218  2ffzeq  10298  flqidz  10466  addmodlteq  10580  frec2uzrand  10587  nninfinf  10625  expcan  10898  nn0opthd  10904  fz1eqb  10972  wrdnval  11061  eqwrd  11071  wrdl1s1  11122  ccatopth  11207  ccatopth2  11208  cj11  11331  sqrt0  11430  recan  11535  0dvds  12237  dvds1  12279  alzdvds  12280  nn0enne  12328  nn0oddm1d2  12335  nnoddm1d2  12336  divalgmod  12353  gcdeq0  12413  algcvgblem  12486  prmexpb  12588  4sqexercise2  12837  4sqlemsdc  12838  4sqlem11  12839  ennnfonelemim  12910  grprcan  13484  grplcan  13509  grpinv11  13516  isnzr2  14061  znidomb  14535  tgdom  14659  en1top  14664  hmeocnvb  14905  metrest  15093  perfect  15588  lgsne0  15630  2lgs  15696  2lgsoddprmlem3  15703  wrdupgren  15807  wrdumgren  15817  bj-nnbist  15880  bj-nnbidc  15893  bj-peano4  16090  bj-nn0sucALT  16113