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  913  pm5.63dc  952  pm4.83dc  957  pm5.71dc  967  19.33b2  1675  19.9t  1688  sb4b  1880  a16gb  1911  euor2  2136  eupickbi  2160  ceqsalg  2828  eqvincg  2927  ddifstab  3336  csbprc  3537  undif4  3554  eqifdc  3639  ifnebibdc  3648  ssprsseq  3830  sssnm  3832  sneqbg  3841  opthpr  3850  elpwuni  4055  ss1o0el1  4281  exmid01  4282  exmidundif  4290  eusv2i  4546  reusv3  4551  iunpw  4571  suc11g  4649  reldmm  4942  ssxpbm  5164  ssxp1  5165  ssxp2  5166  xp11m  5167  2elresin  5434  mpteqb  5725  f1fveq  5896  f1elima  5897  f1imass  5898  fliftf  5923  nnsucuniel  6641  iserd  6706  ecopovtrn  6779  ecopover  6780  ecopovtrng  6782  ecopoverg  6783  map0g  6835  fopwdom  6997  f1finf1o  7114  mkvprop  7325  addcanpig  7521  mulcanpig  7522  srpospr  7970  readdcan  8286  cnegexlem1  8321  addcan  8326  addcan2  8327  neg11  8397  negreb  8411  add20  8621  cru  8749  mulcanapd  8808  uz11  9745  eqreznegel  9809  lbzbi  9811  xneg11  10030  xnn0xadd0  10063  xsubge0  10077  elioc2  10132  elico2  10133  elicc2  10134  fzopth  10257  2ffzeq  10337  flqidz  10506  addmodlteq  10620  frec2uzrand  10627  nninfinf  10665  expcan  10938  nn0opthd  10944  fz1eqb  11012  wrdnval  11102  eqwrd  11112  wrdl1s1  11163  ccatopth  11248  ccatopth2  11249  cj11  11416  sqrt0  11515  recan  11620  0dvds  12322  dvds1  12364  alzdvds  12365  nn0enne  12413  nn0oddm1d2  12420  nnoddm1d2  12421  divalgmod  12438  gcdeq0  12498  algcvgblem  12571  prmexpb  12673  4sqexercise2  12922  4sqlemsdc  12923  4sqlem11  12924  ennnfonelemim  12995  grprcan  13570  grplcan  13595  grpinv11  13602  isnzr2  14148  znidomb  14622  tgdom  14746  en1top  14751  hmeocnvb  14992  metrest  15180  perfect  15675  lgsne0  15717  2lgs  15783  2lgsoddprmlem3  15790  wrdupgren  15896  wrdumgren  15906  usgrausgrben  15970  upgriswlkdc  16071  bj-nnbist  16108  bj-nnbidc  16121  bj-peano4  16318  bj-nn0sucALT  16341