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  2291  rexbiia  2548  reubiia  2720  rmobiia  2725  rabbiia  2789  ceqsrexbv  2938  euxfrdc  2993  eldifpr  3700  eldiftp  3719  eldifsn  3804  elrint  3973  elriin  4046  opeqsn  4351  rabxp  4769  eliunxp  4875  restidsing  5075  ressn  5284  fncnv  5403  dff1o5  5601  respreima  5783  dff4im  5801  dffo3  5802  f1ompt  5806  fsn  5827  fconst3m  5881  fconst4m  5882  eufnfv  5895  dff13  5919  f1mpt  5922  isores2  5964  isoini  5969  eloprabga  6118  mpomptx  6122  resoprab  6127  ov6g  6170  dfopab2  6361  dfoprab3s  6362  dfoprab3  6363  f1od2  6409  brtpos2  6460  dftpos3  6471  tpostpos  6473  dfsmo2  6496  elixp2  6914  mapsnen  7029  xpcomco  7053  eqinfti  7262  dfplpq2  7617  dfmpq2  7618  enq0enq  7694  nqnq0a  7717  nqnq0m  7718  genpassl  7787  genpassu  7788  axsuploc  8294  recexre  8800  recexgt0  8802  reapmul1  8817  apsqgt0  8823  apreim  8825  recexaplem2  8874  rerecclap  8952  elznn0  9538  elznn  9539  msqznn  9624  eluz2b1  9879  eluz2b3  9882  qreccl  9920  rpnegap  9965  elfz2nn0  10392  elfzo3  10444  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  qexpclz  10868  shftidt2  11455  clim0  11908  iser3shft  11969  summodclem3  12004  fprod2dlemstep  12246  eftlub  12314  ndvdsadd  12555  algfx  12687  isprm3  12753  isprm5  12777  xpsfrnel  13490  isabl2  13944  dvdsrcl2  14177  unitinvcl  14201  unitinvinv  14202  unitlinv  14204  unitrinv  14205  isrim  14247  isnzr2  14262  islmod  14370  isridl  14583  cnfldui  14668  ssntr  14916  tx1cn  15063  tx2cn  15064  pilem1  15573  lgsdir2lem4  15833