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  2237  rexbiia  2492  reubiia  2662  rmobiia  2667  rabbiia  2723  ceqsrexbv  2869  euxfrdc  2924  eldifpr  3620  eldiftp  3639  eldifsn  3720  elrint  3885  elriin  3958  opeqsn  4253  rabxp  4664  eliunxp  4767  restidsing  4964  ressn  5170  fncnv  5283  dff1o5  5471  respreima  5645  dff4im  5663  dffo3  5664  f1ompt  5668  fsn  5689  fconst3m  5736  fconst4m  5737  eufnfv  5748  dff13  5769  f1mpt  5772  isores2  5814  isoini  5819  eloprabga  5962  mpomptx  5966  resoprab  5971  ov6g  6012  dfopab2  6190  dfoprab3s  6191  dfoprab3  6192  f1od2  6236  brtpos2  6252  dftpos3  6263  tpostpos  6265  dfsmo2  6288  elixp2  6702  mapsnen  6811  xpcomco  6826  eqinfti  7019  dfplpq2  7353  dfmpq2  7354  enq0enq  7430  nqnq0a  7453  nqnq0m  7454  genpassl  7523  genpassu  7524  axsuploc  8030  recexre  8535  recexgt0  8537  reapmul1  8552  apsqgt0  8558  apreim  8560  recexaplem2  8609  rerecclap  8687  elznn0  9268  elznn  9269  msqznn  9353  eluz2b1  9601  eluz2b3  9604  qreccl  9642  rpnegap  9686  elfz2nn0  10112  elfzo3  10163  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  qexpclz  10541  shftidt2  10841  clim0  11293  iser3shft  11354  summodclem3  11388  fprod2dlemstep  11630  eftlub  11698  ndvdsadd  11936  algfx  12052  isprm3  12118  isprm5  12142  xpsfrnel  12763  isabl2  13097  dvdsrcl2  13268  unitinvcl  13292  unitinvinv  13293  unitlinv  13295  unitrinv  13296  islmod  13381  ssntr  13625  tx1cn  13772  tx2cn  13773  pilem1  14203  lgsdir2lem4  14435