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  2141  eupickbi  2165  ceqsalg  2844  eqvincg  2944  ddifstab  3355  csbprc  3558  undif4  3575  eqifdc  3663  ifnebibdc  3672  ssprsseq  3861  sssnm  3863  sneqbg  3872  opthpr  3881  elpwuni  4086  ss1o0el1  4315  exmid01  4316  exmidundif  4324  eusv2i  4581  reusv3  4586  iunpw  4606  suc11g  4684  reldmm  4980  ssxpbm  5203  ssxp1  5204  ssxp2  5205  xp11m  5206  2elresin  5474  mpteqb  5773  f1fveq  5951  f1elima  5952  f1imass  5953  fliftf  5978  nnsucuniel  6741  iserd  6806  ecopovtrn  6879  ecopover  6880  ecopovtrng  6882  ecopoverg  6883  map0g  6935  fopwdom  7102  f1finf1o  7230  mkvprop  7462  addcanpig  7665  mulcanpig  7666  srpospr  8114  readdcan  8429  cnegexlem1  8464  addcan  8469  addcan2  8470  neg11  8540  negreb  8554  add20  8765  cru  8893  mulcanapd  8952  uz11  9895  eqreznegel  9964  lbzbi  9966  xneg11  10186  xnn0xadd0  10219  xsubge0  10233  elioc2  10288  elico2  10289  elicc2  10290  fzopth  10416  2ffzeq  10497  flqidz  10670  addmodlteq  10784  frec2uzrand  10791  nninfinf  10829  resq01  11044  expcan  11103  nn0opthd  11109  fz1eqb  11178  wrdnval  11280  eqwrd  11290  ccatalpha  11326  wrdl1s1  11343  ccatopth  11433  ccatopth2  11434  cj11  11615  sqrt0  11714  recan  11819  0dvds  12522  dvds1  12564  alzdvds  12565  nn0enne  12613  nn0oddm1d2  12620  nnoddm1d2  12621  divalgmod  12638  gcdeq0  12698  algcvgblem  12771  prmexpb  12873  4sqexercise2  13122  4sqlemsdc  13123  4sqlem11  13124  ennnfonelemim  13259  grprcan  13792  grplcan  13817  grpinv11  13824  isnzr2  14429  znidomb  14932  tgdom  15063  en1top  15068  hmeocnvb  15309  metrest  15497  pellexlem3  15973  perfect  15995  lgsne0  16037  2lgs  16103  2lgsoddprmlem3  16110  wrdupgren  16217  wrdumgren  16227  usgrausgrben  16293  upgriswlkdc  16481  bj-nnbist  16642  bj-nnbidc  16655  bj-peano4  16851  bj-nn0sucALT  16874