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  2648  reubiia  2797  rmobiia  2802  rabbiia  2850  ceqsrexbv  2974  euxfr  3023  2reu5  3045  eldif  3222  dfpss3  3356  elimif  3692  eldifsn  3840  elrint  3968  elriin  4039  ltfinex  4465  dfevenfin2  4513  dfoddfin2  4514  opeq  4620  setconslem6  4737  rabxp  4815  eliunxp  4822  elres  4996  fncnv  5159  dff1o5  5296  respreima  5411  dff4  5422  dffo3  5423  fsn  5433  fconst3  5458  fconst4  5459  dff13  5472  isores2  5494  isoini  5498  eloprabga  5579  resoprab  5582  fnov  5592  ov6g  5601  mpt2mptx  5709  txpcofun  5804  addcfnex  5825  brpprod  5840  tcfnex  6245  addccan2nclem1  6264  nchoicelem16  6305  nchoicelem18  6307