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  2885  ddifstab  3292  csbprc  3493  undif4  3510  eqifdc  3593  ifnebibdc  3601  sssnm  3781  sneqbg  3790  opthpr  3799  elpwuni  4003  ss1o0el1  4227  exmid01  4228  exmidundif  4236  eusv2i  4487  reusv3  4492  iunpw  4512  suc11g  4590  ssxpbm  5102  ssxp1  5103  ssxp2  5104  xp11m  5105  2elresin  5366  mpteqb  5649  f1fveq  5816  f1elima  5817  f1imass  5818  fliftf  5843  nnsucuniel  6550  iserd  6615  ecopovtrn  6688  ecopover  6689  ecopovtrng  6691  ecopoverg  6692  map0g  6744  fopwdom  6894  f1finf1o  7008  mkvprop  7219  addcanpig  7396  mulcanpig  7397  srpospr  7845  readdcan  8161  cnegexlem1  8196  addcan  8201  addcan2  8202  neg11  8272  negreb  8286  add20  8495  cru  8623  mulcanapd  8682  uz11  9618  eqreznegel  9682  lbzbi  9684  xneg11  9903  xnn0xadd0  9936  xsubge0  9950  elioc2  10005  elico2  10006  elicc2  10007  fzopth  10130  2ffzeq  10210  flqidz  10358  addmodlteq  10472  frec2uzrand  10479  nninfinf  10517  expcan  10790  nn0opthd  10796  fz1eqb  10864  wrdnval  10947  eqwrd  10957  cj11  11052  sqrt0  11151  recan  11256  0dvds  11957  dvds1  11998  alzdvds  11999  nn0enne  12046  nn0oddm1d2  12053  nnoddm1d2  12054  divalgmod  12071  gcdeq0  12117  algcvgblem  12190  prmexpb  12292  4sqexercise2  12540  4sqlemsdc  12541  4sqlem11  12542  ennnfonelemim  12584  grprcan  13112  grplcan  13137  grpinv11  13144  isnzr2  13683  znidomb  14157  tgdom  14251  en1top  14256  hmeocnvb  14497  metrest  14685  lgsne0  15195  2lgs  15261  2lgsoddprmlem3  15268  bj-nnbist  15306  bj-nnbidc  15319  bj-peano4  15517  bj-nn0sucALT  15540