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  2661  rmobiia  2666  rabbiia  2722  ceqsrexbv  2868  euxfrdc  2923  eldifpr  3619  eldiftp  3638  eldifsn  3719  elrint  3884  elriin  3956  opeqsn  4251  rabxp  4662  eliunxp  4765  restidsing  4962  ressn  5168  fncnv  5281  dff1o5  5469  respreima  5643  dff4im  5661  dffo3  5662  f1ompt  5666  fsn  5687  fconst3m  5734  fconst4m  5735  eufnfv  5745  dff13  5766  f1mpt  5769  isores2  5811  isoini  5816  eloprabga  5959  mpomptx  5963  resoprab  5968  ov6g  6009  dfopab2  6187  dfoprab3s  6188  dfoprab3  6189  f1od2  6233  brtpos2  6249  dftpos3  6260  tpostpos  6262  dfsmo2  6285  elixp2  6699  mapsnen  6808  xpcomco  6823  eqinfti  7016  dfplpq2  7350  dfmpq2  7351  enq0enq  7427  nqnq0a  7450  nqnq0m  7451  genpassl  7520  genpassu  7521  axsuploc  8026  recexre  8531  recexgt0  8533  reapmul1  8548  apsqgt0  8554  apreim  8556  recexaplem2  8605  rerecclap  8683  elznn0  9264  elznn  9265  msqznn  9349  eluz2b1  9597  eluz2b3  9600  qreccl  9638  rpnegap  9682  elfz2nn0  10107  elfzo3  10158  frecuzrdgtcl  10407  frecuzrdgfunlem  10414  qexpclz  10536  shftidt2  10834  clim0  11286  iser3shft  11347  summodclem3  11381  fprod2dlemstep  11623  eftlub  11691  ndvdsadd  11928  algfx  12044  isprm3  12110  isprm5  12134  isabl2  13028  dvdsrcl2  13199  unitinvcl  13223  unitinvinv  13224  unitlinv  13226  unitrinv  13227  ssntr  13493  tx1cn  13640  tx2cn  13641  pilem1  14071  lgsdir2lem4  14303