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  920  pm5.63dc  959  pm4.83dc  964  pm5.71dc  974  19.33b2  1682  19.9t  1695  sb4b  1887  a16gb  1918  euor2  2145  eupickbi  2169  ceqsalg  2850  eqvincg  2950  ddifstab  3361  csbprc  3571  undif4  3586  eqifdc  3674  ifnebibdc  3683  ssprsseq  3872  sssnm  3874  sneqbg  3883  opthpr  3892  elpwuni  4097  ss1o0el1  4329  exmid01  4330  exmidundif  4338  eusv2i  4596  reusv3  4601  iunpw  4621  suc11g  4699  reldmm  4995  ssxpbm  5218  ssxp1  5219  ssxp2  5220  xp11m  5221  2elresin  5489  mpteqb  5790  f1fveq  5968  f1elima  5969  f1imass  5970  fliftf  5995  nnsucuniel  6758  iserd  6823  ecopovtrn  6896  ecopover  6897  ecopovtrng  6899  ecopoverg  6900  mapfset  6935  map0g  6959  fopwdom  7126  f1finf1o  7254  mkvprop  7488  addcanpig  7691  mulcanpig  7692  srpospr  8140  readdcan  8456  cnegexlem1  8491  addcan  8496  addcan2  8497  neg11  8567  negreb  8581  add20  8792  cru  8920  mulcanapd  8979  uz11  9924  eqreznegel  9993  lbzbi  9995  xneg11  10215  xnn0xadd0  10248  xsubge0  10262  elioc2  10317  elico2  10318  elicc2  10319  fzopth  10445  2ffzeq  10526  flqidz  10699  addmodlteq  10813  frec2uzrand  10820  nninfinf  10858  resq01  11073  expcan  11132  nn0opthd  11138  fz1eqb  11207  wrdnval  11313  eqwrd  11323  ccatalpha  11359  wrdl1s1  11376  ccatopth  11466  ccatopth2  11467  sq01  11638  cj11  11649  sqrt0  11748  recan  11853  0dvds  12556  dvds1  12598  alzdvds  12599  nn0enne  12647  nn0oddm1d2  12654  nnoddm1d2  12655  divalgmod  12672  gcdeq0  12732  algcvgblem  12805  prmexpb  12907  4sqexercise2  13156  4sqlemsdc  13157  4sqlem11  13158  ennnfonelemim  13293  grprcan  13819  grplcan  13844  grpinv11  13851  isnzr2  14464  znidomb  14965  tgdom  15096  en1top  15101  hmeocnvb  15342  metrest  15530  pellexlem3  16007  perfect  16029  lgsne0  16071  2lgs  16137  2lgsoddprmlem3  16144  wrdupgren  16251  wrdumgren  16261  usgrausgrben  16327  upgriswlkdc  16515  bj-nnbist  16686  bj-nnbidc  16699  bj-peano4  16895  bj-nn0sucALT  16918