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  916  pm5.63dc  955  pm4.83dc  960  pm5.71dc  970  19.33b2  1678  19.9t  1691  sb4b  1883  a16gb  1914  euor2  2139  eupickbi  2163  ceqsalg  2842  eqvincg  2941  ddifstab  3351  csbprc  3554  undif4  3571  eqifdc  3659  ifnebibdc  3668  ssprsseq  3856  sssnm  3858  sneqbg  3867  opthpr  3876  elpwuni  4081  ss1o0el1  4310  exmid01  4311  exmidundif  4319  eusv2i  4576  reusv3  4581  iunpw  4601  suc11g  4679  reldmm  4975  ssxpbm  5198  ssxp1  5199  ssxp2  5200  xp11m  5201  2elresin  5469  mpteqb  5768  f1fveq  5945  f1elima  5946  f1imass  5947  fliftf  5972  nnsucuniel  6728  iserd  6793  ecopovtrn  6866  ecopover  6867  ecopovtrng  6869  ecopoverg  6870  map0g  6922  fopwdom  7089  f1finf1o  7217  mkvprop  7449  addcanpig  7649  mulcanpig  7650  srpospr  8098  readdcan  8413  cnegexlem1  8448  addcan  8453  addcan2  8454  neg11  8524  negreb  8538  add20  8748  cru  8876  mulcanapd  8935  uz11  9877  eqreznegel  9946  lbzbi  9948  xneg11  10167  xnn0xadd0  10200  xsubge0  10214  elioc2  10269  elico2  10270  elicc2  10271  fzopth  10395  2ffzeq  10475  flqidz  10646  addmodlteq  10760  frec2uzrand  10767  nninfinf  10805  expcan  11078  nn0opthd  11084  fz1eqb  11153  wrdnval  11255  eqwrd  11265  ccatalpha  11301  wrdl1s1  11318  ccatopth  11408  ccatopth2  11409  cj11  11590  sqrt0  11689  recan  11794  0dvds  12497  dvds1  12539  alzdvds  12540  nn0enne  12588  nn0oddm1d2  12595  nnoddm1d2  12596  divalgmod  12613  gcdeq0  12673  algcvgblem  12746  prmexpb  12848  4sqexercise2  13097  4sqlemsdc  13098  4sqlem11  13099  ennnfonelemim  13175  grprcan  13750  grplcan  13775  grpinv11  13782  isnzr2  14329  znidomb  14806  tgdom  14937  en1top  14942  hmeocnvb  15183  metrest  15371  pellexlem3  15847  perfect  15869  lgsne0  15911  2lgs  15977  2lgsoddprmlem3  15984  wrdupgren  16091  wrdumgren  16101  usgrausgrben  16167  upgriswlkdc  16355  bj-nnbist  16516  bj-nnbidc  16529  bj-peano4  16725  bj-nn0sucALT  16748