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  2200  rexbiia  2453  reubiia  2618  rmobiia  2623  rabbiia  2674  ceqsrexbv  2820  euxfrdc  2874  eldifpr  3559  eldiftp  3577  eldifsn  3658  elrint  3819  elriin  3891  opeqsn  4182  rabxp  4584  eliunxp  4686  ressn  5087  fncnv  5197  dff1o5  5384  respreima  5556  dff4im  5574  dffo3  5575  f1ompt  5579  fsn  5600  fconst3m  5647  fconst4m  5648  eufnfv  5656  dff13  5677  f1mpt  5680  isores2  5722  isoini  5727  eloprabga  5866  mpomptx  5870  resoprab  5875  ov6g  5916  dfopab2  6095  dfoprab3s  6096  dfoprab3  6097  f1od2  6140  brtpos2  6156  dftpos3  6167  tpostpos  6169  dfsmo2  6192  elixp2  6604  mapsnen  6713  xpcomco  6728  eqinfti  6915  dfplpq2  7186  dfmpq2  7187  enq0enq  7263  nqnq0a  7286  nqnq0m  7287  genpassl  7356  genpassu  7357  axsuploc  7861  recexre  8364  recexgt0  8366  reapmul1  8381  apsqgt0  8387  apreim  8389  recexaplem2  8437  rerecclap  8514  elznn0  9093  elznn  9094  msqznn  9175  eluz2b1  9422  eluz2b3  9425  qreccl  9461  rpnegap  9503  elfz2nn0  9923  elfzo3  9971  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  qexpclz  10345  shftidt2  10636  clim0  11086  iser3shft  11147  summodclem3  11181  eftlub  11433  ndvdsadd  11664  algfx  11769  isprm3  11835  ssntr  12330  tx1cn  12477  tx2cn  12478  pilem1  12908