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  1643  19.9t  1656  sb4b  1848  a16gb  1879  euor2  2103  eupickbi  2127  ceqsalg  2791  eqvincg  2888  ddifstab  3295  csbprc  3496  undif4  3513  eqifdc  3596  ifnebibdc  3604  sssnm  3784  sneqbg  3793  opthpr  3802  elpwuni  4006  ss1o0el1  4230  exmid01  4231  exmidundif  4239  eusv2i  4490  reusv3  4495  iunpw  4515  suc11g  4593  ssxpbm  5105  ssxp1  5106  ssxp2  5107  xp11m  5108  2elresin  5369  mpteqb  5652  f1fveq  5819  f1elima  5820  f1imass  5821  fliftf  5846  nnsucuniel  6553  iserd  6618  ecopovtrn  6691  ecopover  6692  ecopovtrng  6694  ecopoverg  6695  map0g  6747  fopwdom  6897  f1finf1o  7013  mkvprop  7224  addcanpig  7401  mulcanpig  7402  srpospr  7850  readdcan  8166  cnegexlem1  8201  addcan  8206  addcan2  8207  neg11  8277  negreb  8291  add20  8501  cru  8629  mulcanapd  8688  uz11  9624  eqreznegel  9688  lbzbi  9690  xneg11  9909  xnn0xadd0  9942  xsubge0  9956  elioc2  10011  elico2  10012  elicc2  10013  fzopth  10136  2ffzeq  10216  flqidz  10376  addmodlteq  10490  frec2uzrand  10497  nninfinf  10535  expcan  10808  nn0opthd  10814  fz1eqb  10882  wrdnval  10965  eqwrd  10975  cj11  11070  sqrt0  11169  recan  11274  0dvds  11976  dvds1  12018  alzdvds  12019  nn0enne  12067  nn0oddm1d2  12074  nnoddm1d2  12075  divalgmod  12092  gcdeq0  12144  algcvgblem  12217  prmexpb  12319  4sqexercise2  12568  4sqlemsdc  12569  4sqlem11  12570  ennnfonelemim  12641  grprcan  13169  grplcan  13194  grpinv11  13201  isnzr2  13740  znidomb  14214  tgdom  14308  en1top  14313  hmeocnvb  14554  metrest  14742  perfect  15237  lgsne0  15279  2lgs  15345  2lgsoddprmlem3  15352  bj-nnbist  15390  bj-nnbidc  15403  bj-peano4  15601  bj-nn0sucALT  15624