Theorem pm5.32i 450

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 449	. 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  451  biadan2  452  anbi2i  453  abai  550  anabs5  563  pm5.33  599  eq2tri  2217  rexbiia  2472  reubiia  2641  rmobiia  2646  rabbiia  2697  ceqsrexbv  2843  euxfrdc  2898  eldifpr  3587  eldiftp  3605  eldifsn  3686  elrint  3847  elriin  3919  opeqsn  4211  rabxp  4620  eliunxp  4722  ressn  5123  fncnv  5233  dff1o5  5420  respreima  5592  dff4im  5610  dffo3  5611  f1ompt  5615  fsn  5636  fconst3m  5683  fconst4m  5684  eufnfv  5692  dff13  5713  f1mpt  5716  isores2  5758  isoini  5763  eloprabga  5902  mpomptx  5906  resoprab  5911  ov6g  5952  dfopab2  6131  dfoprab3s  6132  dfoprab3  6133  f1od2  6176  brtpos2  6192  dftpos3  6203  tpostpos  6205  dfsmo2  6228  elixp2  6640  mapsnen  6749  xpcomco  6764  eqinfti  6956  dfplpq2  7257  dfmpq2  7258  enq0enq  7334  nqnq0a  7357  nqnq0m  7358  genpassl  7427  genpassu  7428  axsuploc  7933  recexre  8436  recexgt0  8438  reapmul1  8453  apsqgt0  8459  apreim  8461  recexaplem2  8509  rerecclap  8586  elznn0  9165  elznn  9166  msqznn  9247  eluz2b1  9494  eluz2b3  9497  qreccl  9533  rpnegap  9575  elfz2nn0  9996  elfzo3  10044  frecuzrdgtcl  10293  frecuzrdgfunlem  10300  qexpclz  10422  shftidt2  10714  clim0  11164  iser3shft  11225  summodclem3  11259  fprod2dlemstep  11501  eftlub  11569  ndvdsadd  11803  algfx  11909  isprm3  11975  ssntr  12482  tx1cn  12629  tx2cn  12630  pilem1  13060