Theorem pm5.32i 618

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

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  pm5.32ri  619  biadan2  623  anbi2i  675  abai  770  anabs5  784  pm5.33  848  2eu8  2291  eq2tri  2412  rexbiia  2647  reubiia  2796  rmobiia  2801  rabbiia  2849  ceqsrexbv  2973  euxfr  3022  2reu5  3044  eldif  3221  dfpss3  3355  elimif  3691  eldifsn  3839  elrint  3967  elriin  4038  ltfinex  4464  dfevenfin2  4512  dfoddfin2  4513  opeq  4619  setconslem6  4736  rabxp  4814  eliunxp  4821  elres  4995  fncnv  5158  dff1o5  5295  respreima  5410  dff4  5421  dffo3  5422  fsn  5432  fconst3  5457  fconst4  5458  dff13  5471  isores2  5493  isoini  5497  eloprabga  5578  resoprab  5581  fnov  5591  ov6g  5600  mpt2mptx  5708  txpcofun  5803  addcfnex  5824  brpprod  5839  tcfnex  6244  addccan2nclem1  6263  nchoicelem16  6304  nchoicelem18  6306