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  2253  rexbiia  2509  reubiia  2679  rmobiia  2684  rabbiia  2745  ceqsrexbv  2891  euxfrdc  2946  eldifpr  3645  eldiftp  3664  eldifsn  3745  elrint  3910  elriin  3983  opeqsn  4281  rabxp  4696  eliunxp  4801  restidsing  4998  ressn  5206  fncnv  5320  dff1o5  5509  respreima  5686  dff4im  5704  dffo3  5705  f1ompt  5709  fsn  5730  fconst3m  5777  fconst4m  5778  eufnfv  5789  dff13  5811  f1mpt  5814  isores2  5856  isoini  5861  eloprabga  6005  mpomptx  6009  resoprab  6014  ov6g  6056  dfopab2  6242  dfoprab3s  6243  dfoprab3  6244  f1od2  6288  brtpos2  6304  dftpos3  6315  tpostpos  6317  dfsmo2  6340  elixp2  6756  mapsnen  6865  xpcomco  6880  eqinfti  7079  dfplpq2  7414  dfmpq2  7415  enq0enq  7491  nqnq0a  7514  nqnq0m  7515  genpassl  7584  genpassu  7585  axsuploc  8092  recexre  8597  recexgt0  8599  reapmul1  8614  apsqgt0  8620  apreim  8622  recexaplem2  8671  rerecclap  8749  elznn0  9332  elznn  9333  msqznn  9417  eluz2b1  9666  eluz2b3  9669  qreccl  9707  rpnegap  9752  elfz2nn0  10178  elfzo3  10230  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  qexpclz  10631  shftidt2  10976  clim0  11428  iser3shft  11489  summodclem3  11523  fprod2dlemstep  11765  eftlub  11833  ndvdsadd  12072  algfx  12190  isprm3  12256  isprm5  12280  xpsfrnel  12927  isabl2  13364  dvdsrcl2  13595  unitinvcl  13619  unitinvinv  13620  unitlinv  13622  unitrinv  13623  isrim  13665  isnzr2  13680  islmod  13787  isridl  14000  cnfldui  14077  ssntr  14290  tx1cn  14437  tx2cn  14438  pilem1  14914  lgsdir2lem4  15147