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  909  pm5.63dc  948  pm4.83dc  953  pm5.71dc  963  19.33b2  1640  19.9t  1653  sb4b  1845  a16gb  1876  euor2  2100  eupickbi  2124  ceqsalg  2788  eqvincg  2884  ddifstab  3291  csbprc  3492  undif4  3509  eqifdc  3592  ifnebibdc  3600  sssnm  3780  sneqbg  3789  opthpr  3798  elpwuni  4002  ss1o0el1  4226  exmid01  4227  exmidundif  4235  eusv2i  4486  reusv3  4491  iunpw  4511  suc11g  4589  ssxpbm  5101  ssxp1  5102  ssxp2  5103  xp11m  5104  2elresin  5365  mpteqb  5648  f1fveq  5815  f1elima  5816  f1imass  5817  fliftf  5842  nnsucuniel  6548  iserd  6613  ecopovtrn  6686  ecopover  6687  ecopovtrng  6689  ecopoverg  6690  map0g  6742  fopwdom  6892  f1finf1o  7006  mkvprop  7217  addcanpig  7394  mulcanpig  7395  srpospr  7843  readdcan  8159  cnegexlem1  8194  addcan  8199  addcan2  8200  neg11  8270  negreb  8284  add20  8493  cru  8621  mulcanapd  8680  uz11  9615  eqreznegel  9679  lbzbi  9681  xneg11  9900  xnn0xadd0  9933  xsubge0  9947  elioc2  10002  elico2  10003  elicc2  10004  fzopth  10127  2ffzeq  10207  flqidz  10355  addmodlteq  10469  frec2uzrand  10476  nninfinf  10514  expcan  10787  nn0opthd  10793  fz1eqb  10861  wrdnval  10944  eqwrd  10954  cj11  11049  sqrt0  11148  recan  11253  0dvds  11954  dvds1  11995  alzdvds  11996  nn0enne  12043  nn0oddm1d2  12050  nnoddm1d2  12051  divalgmod  12068  gcdeq0  12114  algcvgblem  12187  prmexpb  12289  4sqexercise2  12537  4sqlemsdc  12538  4sqlem11  12539  ennnfonelemim  12581  grprcan  13109  grplcan  13134  grpinv11  13141  isnzr2  13680  znidomb  14146  tgdom  14240  en1top  14245  hmeocnvb  14486  metrest  14674  lgsne0  15154  2lgsoddprmlem3  15199  bj-nnbist  15236  bj-nnbidc  15249  bj-peano4  15447  bj-nn0sucALT  15470