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  2267  rexbiia  2523  reubiia  2694  rmobiia  2699  rabbiia  2761  ceqsrexbv  2911  euxfrdc  2966  eldifpr  3670  eldiftp  3689  eldifsn  3771  elrint  3939  elriin  4012  opeqsn  4315  rabxp  4730  eliunxp  4835  restidsing  5034  ressn  5242  fncnv  5359  dff1o5  5553  respreima  5731  dff4im  5749  dffo3  5750  f1ompt  5754  fsn  5775  fconst3m  5826  fconst4m  5827  eufnfv  5838  dff13  5860  f1mpt  5863  isores2  5905  isoini  5910  eloprabga  6055  mpomptx  6059  resoprab  6064  ov6g  6107  dfopab2  6298  dfoprab3s  6299  dfoprab3  6300  f1od2  6344  brtpos2  6360  dftpos3  6371  tpostpos  6373  dfsmo2  6396  elixp2  6812  mapsnen  6927  xpcomco  6946  eqinfti  7148  dfplpq2  7502  dfmpq2  7503  enq0enq  7579  nqnq0a  7602  nqnq0m  7603  genpassl  7672  genpassu  7673  axsuploc  8180  recexre  8686  recexgt0  8688  reapmul1  8703  apsqgt0  8709  apreim  8711  recexaplem2  8760  rerecclap  8838  elznn0  9422  elznn  9423  msqznn  9508  eluz2b1  9757  eluz2b3  9760  qreccl  9798  rpnegap  9843  elfz2nn0  10269  elfzo3  10321  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  qexpclz  10742  shftidt2  11258  clim0  11711  iser3shft  11772  summodclem3  11806  fprod2dlemstep  12048  eftlub  12116  ndvdsadd  12357  algfx  12489  isprm3  12555  isprm5  12579  xpsfrnel  13291  isabl2  13745  dvdsrcl2  13976  unitinvcl  14000  unitinvinv  14001  unitlinv  14003  unitrinv  14004  isrim  14046  isnzr2  14061  islmod  14168  isridl  14381  cnfldui  14466  ssntr  14709  tx1cn  14856  tx2cn  14857  pilem1  15366  lgsdir2lem4  15623