Theorem pm5.32i 451

Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)

Hypothesis

Ref	Expression
pm5.32i.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
pm5.32i	|- ( ( ph /\ ps ) <-> ( ph /\ ch ) )

Proof of Theorem pm5.32i

Step	Hyp	Ref	Expression
1		pm5.32i.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		pm5.32 450	. 2 |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
3	1, 2	mpbi 144	1 |- ( ( ph /\ ps ) <-> ( ph /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.32ri  452  biadan2  453  anbi2i  454  abai  555  anabs5  568  pm5.33  604  eq2tri  2230  rexbiia  2485  reubiia  2654  rmobiia  2659  rabbiia  2715  ceqsrexbv  2861  euxfrdc  2916  eldifpr  3610  eldiftp  3629  eldifsn  3710  elrint  3871  elriin  3943  opeqsn  4237  rabxp  4648  eliunxp  4750  ressn  5151  fncnv  5264  dff1o5  5451  respreima  5624  dff4im  5642  dffo3  5643  f1ompt  5647  fsn  5668  fconst3m  5715  fconst4m  5716  eufnfv  5726  dff13  5747  f1mpt  5750  isores2  5792  isoini  5797  eloprabga  5940  mpomptx  5944  resoprab  5949  ov6g  5990  dfopab2  6168  dfoprab3s  6169  dfoprab3  6170  f1od2  6214  brtpos2  6230  dftpos3  6241  tpostpos  6243  dfsmo2  6266  elixp2  6680  mapsnen  6789  xpcomco  6804  eqinfti  6997  dfplpq2  7316  dfmpq2  7317  enq0enq  7393  nqnq0a  7416  nqnq0m  7417  genpassl  7486  genpassu  7487  axsuploc  7992  recexre  8497  recexgt0  8499  reapmul1  8514  apsqgt0  8520  apreim  8522  recexaplem2  8570  rerecclap  8647  elznn0  9227  elznn  9228  msqznn  9312  eluz2b1  9560  eluz2b3  9563  qreccl  9601  rpnegap  9643  elfz2nn0  10068  elfzo3  10119  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  qexpclz  10497  shftidt2  10796  clim0  11248  iser3shft  11309  summodclem3  11343  fprod2dlemstep  11585  eftlub  11653  ndvdsadd  11890  algfx  12006  isprm3  12072  isprm5  12096  ssntr  12916  tx1cn  13063  tx2cn  13064  pilem1  13494  lgsdir2lem4  13726