Theorem pm5.32i 442

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

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.32ri  443  biadan2  444  anbi2i  445  abai  527  anabs5  540  pm5.33  576  eq2tri  2147  rexbiia  2393  reubiia  2551  rmobiia  2556  rabbiia  2604  ceqsrexbv  2748  euxfrdc  2801  eldifsn  3567  elrint  3728  elriin  3800  opeqsn  4079  rabxp  4474  eliunxp  4575  ressn  4971  fncnv  5080  dff1o5  5262  respreima  5427  dff4im  5445  dffo3  5446  f1ompt  5450  fsn  5469  fconst3m  5516  fconst4m  5517  eufnfv  5525  dff13  5547  f1mpt  5550  isores2  5592  isoini  5597  eloprabga  5735  mpt2mptx  5739  resoprab  5741  ov6g  5782  dfopab2  5959  dfoprab3s  5960  dfoprab3  5961  f1od2  6000  brtpos2  6016  dftpos3  6027  tpostpos  6029  dfsmo2  6052  mapsnen  6526  xpcomco  6540  eqinfti  6713  dfplpq2  6911  dfmpq2  6912  enq0enq  6988  nqnq0a  7011  nqnq0m  7012  genpassl  7081  genpassu  7082  recexre  8053  recexgt0  8055  reapmul1  8070  apsqgt0  8076  apreim  8078  recexaplem2  8119  rerecclap  8195  elznn0  8763  elznn  8764  msqznn  8844  eluz2b1  9086  eluz2b3  9089  qreccl  9125  rpnegap  9164  elfz2nn0  9522  elfzo3  9570  frecuzrdgtcl  9815  frecuzrdgfunlem  9822  qexpclz  9972  shftidt2  10262  clim0  10669  iser3shft  10731  isummolem3  10766  eftlub  10976  ndvdsadd  11205  ialgfx  11308  isprm3  11374