Theorem impbid1 142

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1	|- ( ph -> ( ps -> ch ) )
impbid1.2	|- ( ch -> ps )

Assertion

Ref	Expression
impbid1	|- ( ph -> ( ps <-> ch ) )

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 |- ( ph -> ( ps -> ch ) )
2		impbid1.2	. . 3 |- ( ch -> ps )
3	2	a1i 9	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	impbid 129	1 |- ( ph -> ( ps <-> ch ) )

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  1882  a16gb  1913  euor2  2138  eupickbi  2162  ceqsalg  2832  eqvincg  2931  ddifstab  3341  csbprc  3542  undif4  3559  eqifdc  3646  ifnebibdc  3655  ssprsseq  3840  sssnm  3842  sneqbg  3851  opthpr  3860  elpwuni  4065  ss1o0el1  4293  exmid01  4294  exmidundif  4302  eusv2i  4558  reusv3  4563  iunpw  4583  suc11g  4661  reldmm  4956  ssxpbm  5179  ssxp1  5180  ssxp2  5181  xp11m  5182  2elresin  5450  mpteqb  5746  f1fveq  5923  f1elima  5924  f1imass  5925  fliftf  5950  nnsucuniel  6706  iserd  6771  ecopovtrn  6844  ecopover  6845  ecopovtrng  6847  ecopoverg  6848  map0g  6900  fopwdom  7065  f1finf1o  7189  mkvprop  7417  addcanpig  7614  mulcanpig  7615  srpospr  8063  readdcan  8378  cnegexlem1  8413  addcan  8418  addcan2  8419  neg11  8489  negreb  8503  add20  8713  cru  8841  mulcanapd  8900  uz11  9840  eqreznegel  9909  lbzbi  9911  xneg11  10130  xnn0xadd0  10163  xsubge0  10177  elioc2  10232  elico2  10233  elicc2  10234  fzopth  10358  2ffzeq  10438  flqidz  10609  addmodlteq  10723  frec2uzrand  10730  nninfinf  10768  expcan  11041  nn0opthd  11047  fz1eqb  11115  wrdnval  11210  eqwrd  11220  ccatalpha  11256  wrdl1s1  11273  ccatopth  11363  ccatopth2  11364  cj11  11545  sqrt0  11644  recan  11749  0dvds  12452  dvds1  12494  alzdvds  12495  nn0enne  12543  nn0oddm1d2  12550  nnoddm1d2  12551  divalgmod  12568  gcdeq0  12628  algcvgblem  12701  prmexpb  12803  4sqexercise2  13052  4sqlemsdc  13053  4sqlem11  13054  ennnfonelemim  13125  grprcan  13700  grplcan  13725  grpinv11  13732  isnzr2  14279  znidomb  14754  tgdom  14883  en1top  14888  hmeocnvb  15129  metrest  15317  pellexlem3  15793  perfect  15815  lgsne0  15857  2lgs  15923  2lgsoddprmlem3  15930  wrdupgren  16037  wrdumgren  16047  usgrausgrben  16113  upgriswlkdc  16301  bj-nnbist  16462  bj-nnbidc  16475  bj-peano4  16671  bj-nn0sucALT  16694