Theorem pm5.32d 709

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

Hypothesis

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

Assertion

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

Proof of Theorem pm5.32d

Step	Hyp	Ref	Expression
1		pm5.32d.1	. 2 |- (ph -> (ps -> (ch <-> th)))
2		pm5.32 706	. 2 |- ((ps -> (ch <-> th)) <-> ((ps /\ ch) <-> (ps /\ th)))
3	1, 2	sylib 215	1 |- (ph -> ((ps /\ ch) <-> (ps /\ th)))

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

This theorem is referenced by:  pm5.32rd 710  pm5.32da 711  cbval2 1698  cbvex2 1699  rabbirdvOLD 2802  dfiun2gOLD 3284  ordpwsuc 3896  ordsucun 3905  cores 4400  isoini 4877  rdglim2 5157  1idpr 6285  map2psrpr 6372  btwnz 7428  icounlem 7581  snunioolem 7583  divccncf 8542  efcltlem2 8567  metcnp 9165  occllem5 10810  rnbra 11678  elfzm11 13604  fzind 13610  isprm2 13775  isprm3 13776  ee7.2aOLD 14262  compfipin0lem 15435  compfipin0 15436  cnoprab1 15921  cnoprab2 15922  txmet 15925  pm14.122b 16387  pm14.123b 16390  rexbidar 16423

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