Theorem impbida 561

Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)

Hypotheses

Ref	Expression
impbida.1	|- ( ( ph /\ ps ) -> ch )
impbida.2	|- ( ( ph /\ ch ) -> ps )

Assertion

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

Proof of Theorem impbida

Step	Hyp	Ref	Expression
1		impbida.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 113	. 2 |- ( ph -> ( ps -> ch ) )
3		impbida.2	. . 3 |- ( ( ph /\ ch ) -> ps )
4	3	ex 113	. 2 |- ( ph -> ( ch -> ps ) )
5	2, 4	impbid 127	1 |- ( ph -> ( ps <-> ch ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> 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:  eqrdav  2081  funfvbrb  5312  f1ocnv2d  5735  1stconst  5873  2ndconst  5874  cnvf1o  5877  ersymb  6186  swoer  6200  erth  6216  enen1  6381  enen2  6382  domen1  6383  domen2  6384  fidifsnen  6405  fundmfibi  6448  f1dmvrnfibi  6452  ordiso2  6505  fzsplit2  9145  fseq1p1m1  9187  elfz2nn0  9205  btwnzge0  9382  modqsubdir  9475  zesq  9688  sizeprg  9832  rereb  9888  abslt  10112  absle  10113  maxleastb  10238  maxltsup  10242  iiserex  10315  dvdsadd2b  10387  nn0ob  10452  dfgcd3  10543  dfgcd2  10547  dvdsmulgcd  10558  lcmgcdeq  10609