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  1882  a16gb  1913  euor2  2138  eupickbi  2162  ceqsalg  2832  eqvincg  2931  ddifstab  3341  csbprc  3542  undif4  3559  eqifdc  3646  ifnebibdc  3655  ssprsseq  3840  sssnm  3842  sneqbg  3851  opthpr  3860  elpwuni  4065  ss1o0el1  4293  exmid01  4294  exmidundif  4302  eusv2i  4558  reusv3  4563  iunpw  4583  suc11g  4661  reldmm  4956  ssxpbm  5179  ssxp1  5180  ssxp2  5181  xp11m  5182  2elresin  5450  mpteqb  5746  f1fveq  5923  f1elima  5924  f1imass  5925  fliftf  5950  nnsucuniel  6706  iserd  6771  ecopovtrn  6844  ecopover  6845  ecopovtrng  6847  ecopoverg  6848  map0g  6900  fopwdom  7065  f1finf1o  7189  mkvprop  7400  addcanpig  7597  mulcanpig  7598  srpospr  8046  readdcan  8361  cnegexlem1  8396  addcan  8401  addcan2  8402  neg11  8472  negreb  8486  add20  8696  cru  8824  mulcanapd  8883  uz11  9823  eqreznegel  9892  lbzbi  9894  xneg11  10113  xnn0xadd0  10146  xsubge0  10160  elioc2  10215  elico2  10216  elicc2  10217  fzopth  10341  2ffzeq  10421  flqidz  10592  addmodlteq  10706  frec2uzrand  10713  nninfinf  10751  expcan  11024  nn0opthd  11030  fz1eqb  11098  wrdnval  11193  eqwrd  11203  ccatalpha  11239  wrdl1s1  11256  ccatopth  11346  ccatopth2  11347  cj11  11528  sqrt0  11627  recan  11732  0dvds  12435  dvds1  12477  alzdvds  12478  nn0enne  12526  nn0oddm1d2  12533  nnoddm1d2  12534  divalgmod  12551  gcdeq0  12611  algcvgblem  12684  prmexpb  12786  4sqexercise2  13035  4sqlemsdc  13036  4sqlem11  13037  ennnfonelemim  13108  grprcan  13683  grplcan  13708  grpinv11  13715  isnzr2  14262  znidomb  14737  tgdom  14866  en1top  14871  hmeocnvb  15112  metrest  15300  pellexlem3  15776  perfect  15798  lgsne0  15840  2lgs  15906  2lgsoddprmlem3  15913  wrdupgren  16020  wrdumgren  16030  usgrausgrben  16096  upgriswlkdc  16284  bj-nnbist  16445  bj-nnbidc  16458  bj-peano4  16654  bj-nn0sucALT  16677