Theorem pm5.32da 647

Description: Distribution of implication over biconditional (deduction rule).

Hypothesis

Ref	Expression
pm5.32da.1	|- ((ph /\ ps) -> (ch <-> th))

Assertion

Ref	Expression
pm5.32da	|- (ph -> ((ps /\ ch) <-> (ps /\ th)))

Proof of Theorem pm5.32da

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 |- ((ph /\ ps) -> (ch <-> th))
2	1	ex 373	. 2 |- (ph -> (ps -> (ch <-> th)))
3	2	pm5.32d 645	1 |- (ph -> ((ps /\ ch) <-> (ps /\ th)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  rexbida 1650  reubidva 1771  rabbidv 1797  reuhyp 2895  fnopabfv 3743  fnrnfv 3744  funiunfv 3851  f1fv 3859  2ndconst 4081  oaabs 4236  mapxpen 4475  xpmapenlem3 4478  xpmapenlem4 4479  xpmapenlem5 4480  aceq6b 4714  brdom7disj 4776  ltexpi 5001  axrnegex 5255  axrrecex 5256  suprleub 6006  nnunb 6017  supxrleub 6046  zrevaddclt 6117  qrevaddclt 6213  2shft 6289  icoshft 6341  sumeq2 6923  bastop2 7585  elcls2 7647  iscncl 7709  cncnp2 7718  blrn3 7787  isopn4 7802  neibl 7817  metcnplem 7825  metcnp2 7827  metcn 7828  metcnp3 7835  cncfmet 7844  bl2ioo 7850  lmclim 7898  metelcls 7900  metcnp4 7904  opr1cn 7912  opr2cn 7913  fsumcnlem 7923  nvmfval 8204  ip1cnilem5 8311  isblo2 8375  htthlem5 8554  h2hlm 8789  pjeqt 9157  adjval2t 9732  brafnmult 9791  kbmult 9795  adjbdlnt 9931  kbass2t 9962  kbass5t 9965

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain