Theorem pm5.32i 441

Description: Distribution of implication over biconditional (inference rule). (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 440	. 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  442  biadan2  443  anbi2i  444  abai  524  anabs5  537  pm5.33  573  eq2tri  2140  rexbiia  2381  reubiia  2538  rmobiia  2543  rabbiia  2591  ceqsrexbv  2726  euxfrdc  2778  eldifsn  3517  elrint  3676  elriin  3748  opeqsn  4007  rabxp  4398  eliunxp  4493  ressn  4878  fncnv  4985  dff1o5  5155  respreima  5316  dff4im  5334  dffo3  5335  f1ompt  5341  fsn  5356  fconst3m  5401  fconst4m  5402  eufnfv  5410  dff13  5428  f1mpt  5431  isores2  5473  isoini  5477  eloprabga  5611  mpt2mptx  5615  resoprab  5617  ov6g  5658  dfopab2  5835  dfoprab3s  5836  dfoprab3  5837  f1od2  5876  brtpos2  5889  dftpos3  5900  tpostpos  5902  dfsmo2  5925  xpcomco  6323  eqinfti  6433  dfplpq2  6544  dfmpq2  6545  enq0enq  6621  nqnq0a  6644  nqnq0m  6645  genpassl  6714  genpassu  6715  recexre  7678  recexgt0  7680  reapmul1  7695  apsqgt0  7701  apreim  7703  recexaplem2  7742  rerecclap  7818  elznn0  8366  elznn  8367  msqznn  8447  eluz2b1  8688  eluz2b3  8691  qreccl  8727  rpnegap  8766  elfz2nn0  9128  elfzo3  9172  frecuzrdgfn  9414  qexpclz  9497  shftidt2  9720  clim0  10124  ndvdsadd  10331  ialgfx  10434  isprm3  10500