Theorem pm5.32i 458

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 457	. 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  459  biadan2  460  anbi2i  461  abai  566  anabs5  579  pm5.33  617  annotanannot  680  eq2tri  2298  rexbiia  2565  reubiia  2738  rmobiia  2743  rabbiia  2807  ceqsrexbv  2957  euxfrdc  3012  eldifpr  3732  eldiftp  3751  eldifsn  3836  elrint  4005  elriin  4078  opeqsn  4388  rabxp  4807  eliunxp  4914  restidsing  5114  ressn  5323  fncnv  5442  dff1o5  5643  respreima  5827  dff4im  5845  dffo3  5846  f1ompt  5850  fsn  5871  fconst3m  5925  fconst4m  5926  eufnfv  5939  dff13  5964  f1mpt  5967  isores2  6009  isoini  6014  eloprabga  6165  mpomptx  6169  resoprab  6174  ov6g  6217  dfopab2  6413  dfoprab3s  6414  dfoprab3  6415  f1od2  6461  brtpos2  6512  dftpos3  6523  tpostpos  6525  dfsmo2  6548  elixp2  6974  mapsnen  7090  xpcomco  7114  eqinfti  7350  dfplpq2  7711  dfmpq2  7712  enq0enq  7788  nqnq0a  7811  nqnq0m  7812  genpassl  7881  genpassu  7882  axsuploc  8388  recexre  8896  recexgt0  8898  reapmul1  8913  apsqgt0  8919  apreim  8921  recexaplem2  8970  rerecclap  9050  elznn0  9638  elznn  9639  msqznn  9725  eluz2b1  9980  eluz2b3  9983  qreccl  10021  rpnegap  10066  elfz2nn0  10497  elfzo3  10549  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  qexpclz  10975  shftidt2  11575  clim0  12029  iser3shft  12090  summodclem3  12125  fprod2dlemstep  12367  eftlub  12435  ndvdsadd  12676  algfx  12808  isprm3  12874  isprm5  12898  ballotfilemodife  13218  xpsfrnel  13642  isabl2  14074  dvdsrcl2  14379  unitinvcl  14403  unitinvinv  14404  unitlinv  14406  unitrinv  14407  isrim  14449  isnzr2  14464  drngprop  14590  islmod  14600  isridl  14813  cnfldui  14896  ssntr  15146  tx1cn  15293  tx2cn  15294  pilem1  15803  lgsdir2lem4  16064