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  910  pm5.63dc  949  pm4.83dc  954  pm5.71dc  964  19.33b2  1652  19.9t  1665  sb4b  1857  a16gb  1888  euor2  2112  eupickbi  2136  ceqsalg  2800  eqvincg  2897  ddifstab  3305  csbprc  3506  undif4  3523  eqifdc  3607  ifnebibdc  3615  sssnm  3795  sneqbg  3804  opthpr  3813  elpwuni  4017  ss1o0el1  4241  exmid01  4242  exmidundif  4250  eusv2i  4502  reusv3  4507  iunpw  4527  suc11g  4605  ssxpbm  5118  ssxp1  5119  ssxp2  5120  xp11m  5121  2elresin  5387  mpteqb  5670  f1fveq  5841  f1elima  5842  f1imass  5843  fliftf  5868  nnsucuniel  6581  iserd  6646  ecopovtrn  6719  ecopover  6720  ecopovtrng  6722  ecopoverg  6723  map0g  6775  fopwdom  6933  f1finf1o  7049  mkvprop  7260  addcanpig  7447  mulcanpig  7448  srpospr  7896  readdcan  8212  cnegexlem1  8247  addcan  8252  addcan2  8253  neg11  8323  negreb  8337  add20  8547  cru  8675  mulcanapd  8734  uz11  9671  eqreznegel  9735  lbzbi  9737  xneg11  9956  xnn0xadd0  9989  xsubge0  10003  elioc2  10058  elico2  10059  elicc2  10060  fzopth  10183  2ffzeq  10263  flqidz  10429  addmodlteq  10543  frec2uzrand  10550  nninfinf  10588  expcan  10861  nn0opthd  10867  fz1eqb  10935  wrdnval  11024  eqwrd  11034  wrdl1s1  11084  cj11  11216  sqrt0  11315  recan  11420  0dvds  12122  dvds1  12164  alzdvds  12165  nn0enne  12213  nn0oddm1d2  12220  nnoddm1d2  12221  divalgmod  12238  gcdeq0  12298  algcvgblem  12371  prmexpb  12473  4sqexercise2  12722  4sqlemsdc  12723  4sqlem11  12724  ennnfonelemim  12795  grprcan  13369  grplcan  13394  grpinv11  13401  isnzr2  13946  znidomb  14420  tgdom  14544  en1top  14549  hmeocnvb  14790  metrest  14978  perfect  15473  lgsne0  15515  2lgs  15581  2lgsoddprmlem3  15588  bj-nnbist  15680  bj-nnbidc  15693  bj-peano4  15891  bj-nn0sucALT  15914