Theorem impbid1 140

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 127	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  impbid2  141  iba  294  ibar  295  pm4.81dc  847  pm5.63dc  887  pm4.83dc  892  pm5.71dc  902  19.33b2  1560  19.9t  1573  sb4b  1755  a16gb  1786  euor2  1999  eupickbi  2023  ceqsalg  2627  eqvincg  2719  ddifstab  3104  csbprc  3289  undif4  3306  sssnm  3546  sneqbg  3555  opthpr  3564  elpwuni  3762  eusv2i  4205  reusv3  4210  iunpw  4229  suc11g  4300  xpid11m  4575  ssxpbm  4776  ssxp1  4777  ssxp2  4778  xp11m  4779  2elresin  5030  mpteqb  5282  f1fveq  5432  f1elima  5433  f1imass  5434  fliftf  5459  iserd  6155  ecopovtrn  6226  ecopover  6227  ecopovtrng  6229  ecopoverg  6230  fopwdom  6333  addcanpig  6524  mulcanpig  6525  srpospr  6959  readdcan  7248  cnegexlem1  7283  addcan  7288  addcan2  7289  neg11  7359  negreb  7373  add20  7578  cru  7702  mulcanapd  7751  uz11  8641  eqreznegel  8699  lbzbi  8701  xneg11  8901  elioc2  8959  elico2  8960  elicc2  8961  fzopth  9079  2ffzeq  9151  flqidz  9288  addmodlteq  9400  frec2uzrand  9407  expcan  9644  nn0opthd  9649  cj11  9792  sqrt0  9890  recan  9995  0dvds  10215  dvds1  10253  alzdvds  10254  nn0enne  10302  nn0oddm1d2  10309  nnoddm1d2  10310  divalgmod  10327  gcdeq0  10368  algcvgblem  10431  prmexpb  10530  bj-peano4  10750  bj-nn0sucALT  10773