Theorem pm5.32da 711

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 402	. 2 |- (ph -> (ps -> (ch <-> th)))
3	2	pm5.32d 709	1 |- (ph -> ((ps /\ ch) <-> (ps /\ th)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  rexbida 2118  reubidva 2259  rabbidva 2286  reuhypd 3848  dffn5 4717  fnrnfv 4718  funiunfv 4842  dff13 4850  oaabs 5309  riotabidva 5575  mapxpen 5589  xpmapenlem3 5592  xpmapenlem4 5593  xpmapenlem5 5594  aceq6b 5904  brdom7disj 5966  ltexpi 6181  axrnegex 6436  axrrecex 6437  suprleub 7268  nnunb 7279  supxrleub 7308  zrevaddcl 7379  qrevaddcl 7455  icoshft 7577  ioojoin 7585  fzsuc 7678  2shfti 7765  sumeq2 8245  bastop2 8913  elcls2 8981  iscnp2 9037  iscncl 9047  cncnp2 9056  blrn3 9124  isopn4 9139  neibl 9154  metcnplem 9164  metcnp2 9166  metcn 9167  metcnp3 9174  cncfmet 9183  bl2ioo 9189  lmclim 9241  metelcls 9243  metcnp4 9248  opr1cn 9256  opr2cn 9257  fsumcnlem 9267  nvmfval 9596  ip1cnilem5 9716  isblo2 9783  htthlem5 9971  uptx 10226  2txcn 10229  h2hlm 10482  pjeq 10875  adjval2 11452  brafnmul 11512  kbmul 11516  adjbdln 11653  kbass2 11688  kbass5 11691  surjsec2 14467  prodeq2 14661  curgrpact 14735  cmprtr 14760  svs2 14829  svs3 14830  iscnp3 14946  fclusnei 15607  isfclusf 15625  fclusfnei 15626  infmrgelb 15766  fzsplit 15792  blssp 15844  cnresima 15891  lmtlm 15908  txmet 15925  pcoass 16085  isdivrng3 16112  isidlc 16163  pltval3 16787  glbconx 17029

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 164  df-an 242

Copyright terms: Public domain