Theorem pm5.32i 458

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 457	. 2 |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
3	1, 2	mpbi 145	1 |- ( ( ph /\ ps ) <-> ( ph /\ ch ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.32ri  459  biadan2  460  anbi2i  461  abai  566  anabs5  579  pm5.33  617  annotanannot  680  eq2tri  2298  rexbiia  2565  reubiia  2738  rmobiia  2743  rabbiia  2807  ceqsrexbv  2957  euxfrdc  3012  eldifpr  3736  eldiftp  3755  eldifsn  3841  elrint  4010  elriin  4083  opeqsn  4395  rabxp  4814  eliunxp  4921  restidsing  5122  ressn  5331  fncnv  5450  dff1o5  5651  respreima  5839  dff4im  5857  dffo3  5858  f1ompt  5862  fsn  5883  fconst3m  5937  fconst4m  5938  eufnfv  5952  dff13  5977  f1mpt  5980  isores2  6022  isoini  6027  eloprabga  6178  mpomptx  6182  resoprab  6187  ov6g  6230  dfopab2  6427  dfoprab3s  6428  dfoprab3  6429  f1od2  6475  brtpos2  6527  dftpos3  6538  tpostpos  6540  dfsmo2  6563  elixp2  6990  mapsnen  7106  xpcomco  7130  eqinfti  7366  dfplpq2  7727  dfmpq2  7728  enq0enq  7804  nqnq0a  7827  nqnq0m  7828  genpassl  7897  genpassu  7898  axsuploc  8404  recexre  8914  recexgt0  8916  reapmul1  8931  apsqgt0  8937  apreim  8939  recexaplem2  8988  rerecclap  9068  elznn0  9668  elznn  9669  msqznn  9756  eluz2b1  10016  eluz2b3  10019  qreccl  10057  rpnegap  10103  elfz2nn0  10535  elfzo3  10587  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  qexpclz  11017  shftidt2  11618  clim0  12075  iser3shft  12136  summodclem3  12171  fprod2dlemstep  12413  eftlub  12481  ndvdsadd  12722  algfx  12854  isprm3  12920  isprm5  12945  ballotfilemodife  13297  xpsfrnel  13723  isabl2  14186  dvdsrcl2  14514  unitinvcl  14538  unitinvinv  14539  unitlinv  14541  unitrinv  14542  isrim  14584  isnzr2  14599  drngprop  14725  islmod  14735  isridl  14949  cnfldui  15032  isassa  15110  mvrclfi  15226  ssntr  15365  tx1cn  15512  tx2cn  15513  pilem1  16023  lgsdir2lem4  16372  alsralrex  17377  dfalseu2  17401