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  annotanannot  676  eq2tri  2292  rexbiia  2557  reubiia  2730  rmobiia  2735  rabbiia  2799  ceqsrexbv  2948  euxfrdc  3003  eldifpr  3716  eldiftp  3735  eldifsn  3820  elrint  3989  elriin  4062  opeqsn  4369  rabxp  4787  eliunxp  4894  restidsing  5094  ressn  5303  fncnv  5422  dff1o5  5623  respreima  5805  dff4im  5823  dffo3  5824  f1ompt  5828  fsn  5849  fconst3m  5903  fconst4m  5904  eufnfv  5917  dff13  5941  f1mpt  5944  isores2  5986  isoini  5991  eloprabga  6140  mpomptx  6144  resoprab  6149  ov6g  6192  dfopab2  6383  dfoprab3s  6384  dfoprab3  6385  f1od2  6431  brtpos2  6482  dftpos3  6493  tpostpos  6495  dfsmo2  6518  elixp2  6937  mapsnen  7053  xpcomco  7077  eqinfti  7311  dfplpq2  7669  dfmpq2  7670  enq0enq  7746  nqnq0a  7769  nqnq0m  7770  genpassl  7839  genpassu  7840  axsuploc  8346  recexre  8852  recexgt0  8854  reapmul1  8869  apsqgt0  8875  apreim  8877  recexaplem2  8926  rerecclap  9004  elznn0  9592  elznn  9593  msqznn  9678  eluz2b1  9933  eluz2b3  9936  qreccl  9974  rpnegap  10019  elfz2nn0  10446  elfzo3  10498  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  qexpclz  10922  shftidt2  11517  clim0  11970  iser3shft  12031  summodclem3  12066  fprod2dlemstep  12308  eftlub  12376  ndvdsadd  12617  algfx  12749  isprm3  12815  isprm5  12839  xpsfrnel  13557  isabl2  14011  dvdsrcl2  14244  unitinvcl  14268  unitinvinv  14269  unitlinv  14271  unitrinv  14272  isrim  14314  isnzr2  14329  islmod  14439  isridl  14652  cnfldui  14737  ssntr  14987  tx1cn  15134  tx2cn  15135  pilem1  15644  lgsdir2lem4  15904