Theorem pm5.32i 454

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 453	. 2 |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
3	1, 2	mpbi 145	1 |- ( ( ph /\ ps ) <-> ( ph /\ ch ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32ri  455  biadan2  456  anbi2i  457  abai  560  anabs5  573  pm5.33  609  eq2tri  2265  rexbiia  2521  reubiia  2691  rmobiia  2696  rabbiia  2757  ceqsrexbv  2904  euxfrdc  2959  eldifpr  3660  eldiftp  3679  eldifsn  3760  elrint  3925  elriin  3998  opeqsn  4297  rabxp  4712  eliunxp  4817  restidsing  5015  ressn  5223  fncnv  5340  dff1o5  5531  respreima  5708  dff4im  5726  dffo3  5727  f1ompt  5731  fsn  5752  fconst3m  5803  fconst4m  5804  eufnfv  5815  dff13  5837  f1mpt  5840  isores2  5882  isoini  5887  eloprabga  6032  mpomptx  6036  resoprab  6041  ov6g  6084  dfopab2  6275  dfoprab3s  6276  dfoprab3  6277  f1od2  6321  brtpos2  6337  dftpos3  6348  tpostpos  6350  dfsmo2  6373  elixp2  6789  mapsnen  6903  xpcomco  6921  eqinfti  7122  dfplpq2  7467  dfmpq2  7468  enq0enq  7544  nqnq0a  7567  nqnq0m  7568  genpassl  7637  genpassu  7638  axsuploc  8145  recexre  8651  recexgt0  8653  reapmul1  8668  apsqgt0  8674  apreim  8676  recexaplem2  8725  rerecclap  8803  elznn0  9387  elznn  9388  msqznn  9473  eluz2b1  9722  eluz2b3  9725  qreccl  9763  rpnegap  9808  elfz2nn0  10234  elfzo3  10286  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  qexpclz  10705  shftidt2  11143  clim0  11596  iser3shft  11657  summodclem3  11691  fprod2dlemstep  11933  eftlub  12001  ndvdsadd  12242  algfx  12374  isprm3  12440  isprm5  12464  xpsfrnel  13176  isabl2  13630  dvdsrcl2  13861  unitinvcl  13885  unitinvinv  13886  unitlinv  13888  unitrinv  13889  isrim  13931  isnzr2  13946  islmod  14053  isridl  14266  cnfldui  14351  ssntr  14594  tx1cn  14741  tx2cn  14742  pilem1  15251  lgsdir2lem4  15508