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  562  anabs5  575  pm5.33  613  eq2tri  2291  rexbiia  2547  reubiia  2719  rmobiia  2724  rabbiia  2788  ceqsrexbv  2937  euxfrdc  2992  eldifpr  3696  eldiftp  3715  eldifsn  3800  elrint  3968  elriin  4041  opeqsn  4345  rabxp  4763  eliunxp  4869  restidsing  5069  ressn  5277  fncnv  5396  dff1o5  5592  respreima  5775  dff4im  5793  dffo3  5794  f1ompt  5798  fsn  5819  fconst3m  5872  fconst4m  5873  eufnfv  5884  dff13  5908  f1mpt  5911  isores2  5953  isoini  5958  eloprabga  6107  mpomptx  6111  resoprab  6116  ov6g  6159  dfopab2  6351  dfoprab3s  6352  dfoprab3  6353  f1od2  6399  brtpos2  6416  dftpos3  6427  tpostpos  6429  dfsmo2  6452  elixp2  6870  mapsnen  6985  xpcomco  7009  eqinfti  7218  dfplpq2  7573  dfmpq2  7574  enq0enq  7650  nqnq0a  7673  nqnq0m  7674  genpassl  7743  genpassu  7744  axsuploc  8251  recexre  8757  recexgt0  8759  reapmul1  8774  apsqgt0  8780  apreim  8782  recexaplem2  8831  rerecclap  8909  elznn0  9493  elznn  9494  msqznn  9579  eluz2b1  9834  eluz2b3  9837  qreccl  9875  rpnegap  9920  elfz2nn0  10346  elfzo3  10398  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  qexpclz  10821  shftidt2  11392  clim0  11845  iser3shft  11906  summodclem3  11940  fprod2dlemstep  12182  eftlub  12250  ndvdsadd  12491  algfx  12623  isprm3  12689  isprm5  12713  xpsfrnel  13426  isabl2  13880  dvdsrcl2  14112  unitinvcl  14136  unitinvinv  14137  unitlinv  14139  unitrinv  14140  isrim  14182  isnzr2  14197  islmod  14304  isridl  14517  cnfldui  14602  ssntr  14845  tx1cn  14992  tx2cn  14993  pilem1  15502  lgsdir2lem4  15759