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  908  pm5.63dc  946  pm4.83dc  951  pm5.71dc  961  19.33b2  1629  19.9t  1642  sb4b  1834  a16gb  1865  euor2  2084  eupickbi  2108  ceqsalg  2766  eqvincg  2862  ddifstab  3268  csbprc  3469  undif4  3486  eqifdc  3570  sssnm  3755  sneqbg  3764  opthpr  3773  elpwuni  3977  ss1o0el1  4198  exmid01  4199  exmidundif  4207  eusv2i  4456  reusv3  4461  iunpw  4481  suc11g  4557  ssxpbm  5065  ssxp1  5066  ssxp2  5067  xp11m  5068  2elresin  5328  mpteqb  5607  f1fveq  5773  f1elima  5774  f1imass  5775  fliftf  5800  nnsucuniel  6496  iserd  6561  ecopovtrn  6632  ecopover  6633  ecopovtrng  6635  ecopoverg  6636  map0g  6688  fopwdom  6836  f1finf1o  6946  mkvprop  7156  addcanpig  7333  mulcanpig  7334  srpospr  7782  readdcan  8097  cnegexlem1  8132  addcan  8137  addcan2  8138  neg11  8208  negreb  8222  add20  8431  cru  8559  mulcanapd  8618  uz11  9550  eqreznegel  9614  lbzbi  9616  xneg11  9834  xnn0xadd0  9867  xsubge0  9881  elioc2  9936  elico2  9937  elicc2  9938  fzopth  10061  2ffzeq  10141  flqidz  10286  addmodlteq  10398  frec2uzrand  10405  expcan  10696  nn0opthd  10702  fz1eqb  10770  cj11  10914  sqrt0  11013  recan  11118  0dvds  11818  dvds1  11859  alzdvds  11860  nn0enne  11907  nn0oddm1d2  11914  nnoddm1d2  11915  divalgmod  11932  gcdeq0  11978  algcvgblem  12049  prmexpb  12151  ennnfonelemim  12425  grprcan  12910  grplcan  12932  grpinv11  12939  tgdom  13575  en1top  13580  hmeocnvb  13821  metrest  14009  lgsne0  14442  2lgsoddprmlem3  14462  bj-nnbist  14499  bj-nnbidc  14512  bj-peano4  14710  bj-nn0sucALT  14733