Theorem pm5.32da 648

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 646	1 |- (ph -> ((ps /\ ch) <-> (ps /\ th)))

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

This theorem is referenced by:  rexbida 1656  reubidva 1777  rabbidv 1803  reuhyp 2901  fnopabfv 3753  fnrnfv 3754  funiunfv 3861  f1fv 3869  2ndconst 4090  oaabs 4245  mapxpen 4484  xpmapenlem3 4487  xpmapenlem4 4488  xpmapenlem5 4489  aceq6b 4725  brdom7disj 4787  ltexpi 5012  axrnegex 5266  axrrecex 5267  suprleub 6016  nnunb 6027  supxrleub 6056  zrevaddclt 6127  qrevaddclt 6225  2shft 6302  icoshft 6354  sumeq2 6938  bastop2 7603  elcls2 7665  iscnp2 7721  iscncl 7730  cncnp2 7739  blrn3 7809  isopn4 7824  neibl 7839  metcnplem 7848  metcnp2 7850  metcn 7851  metcnp3 7858  cncfmet 7867  bl2ioo 7873  lmclim 7925  metelcls 7927  metcnp4 7932  opr1cn 7940  opr2cn 7941  fsumcnlem 7951  nvmfval 8228  ip1cnilem5 8339  isblo2 8403  htthlem5 8582  h2hlm 8805  pjeqt 9197  adjval2t 9772  brafnmult 9832  kbmult 9836  adjbdlnt 9972  kbass2t 10006  kbass5t 10009

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