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  611  eq2tri  2289  rexbiia  2545  reubiia  2717  rmobiia  2722  rabbiia  2784  ceqsrexbv  2934  euxfrdc  2989  eldifpr  3693  eldiftp  3712  eldifsn  3794  elrint  3962  elriin  4035  opeqsn  4338  rabxp  4755  eliunxp  4860  restidsing  5060  ressn  5268  fncnv  5386  dff1o5  5580  respreima  5762  dff4im  5780  dffo3  5781  f1ompt  5785  fsn  5806  fconst3m  5857  fconst4m  5858  eufnfv  5869  dff13  5891  f1mpt  5894  isores2  5936  isoini  5941  eloprabga  6090  mpomptx  6094  resoprab  6099  ov6g  6142  dfopab2  6333  dfoprab3s  6334  dfoprab3  6335  f1od2  6379  brtpos2  6395  dftpos3  6406  tpostpos  6408  dfsmo2  6431  elixp2  6847  mapsnen  6962  xpcomco  6981  eqinfti  7183  dfplpq2  7537  dfmpq2  7538  enq0enq  7614  nqnq0a  7637  nqnq0m  7638  genpassl  7707  genpassu  7708  axsuploc  8215  recexre  8721  recexgt0  8723  reapmul1  8738  apsqgt0  8744  apreim  8746  recexaplem2  8795  rerecclap  8873  elznn0  9457  elznn  9458  msqznn  9543  eluz2b1  9792  eluz2b3  9795  qreccl  9833  rpnegap  9878  elfz2nn0  10304  elfzo3  10356  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  qexpclz  10777  shftidt2  11338  clim0  11791  iser3shft  11852  summodclem3  11886  fprod2dlemstep  12128  eftlub  12196  ndvdsadd  12437  algfx  12569  isprm3  12635  isprm5  12659  xpsfrnel  13372  isabl2  13826  dvdsrcl2  14057  unitinvcl  14081  unitinvinv  14082  unitlinv  14084  unitrinv  14085  isrim  14127  isnzr2  14142  islmod  14249  isridl  14462  cnfldui  14547  ssntr  14790  tx1cn  14937  tx2cn  14938  pilem1  15447  lgsdir2lem4  15704