Theorem pm5.32d 491

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 488	. 2 |- ((ps -> (ch <-> th)) <-> ((ps /\ ch) <-> (ps /\ th)))
3	1, 2	sylib 173	1 |- (ph -> ((ps /\ ch) <-> (ps /\ th)))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  pm5.32rd 492  cbval2 974  cbvex2 975  birexda 1214  bireudva 1317  birabdv 1343  reuhyp 1581  birabrdv 1648  onpwsuc 2315  ordsucun 2333  fnopabfv 2858  fniunfv 2860  f1fv 2916  isoini 2938  rdglim2 2987  mapxpen 3390  xpmapenlem3 3393  xpmapenlem4 3394  xpmapenlem5 3395  aceq6b 3565  ltexpi 3823  1idpr 3927  map2psrpr 4014  axrnegex 4080  axrrecex 4081  nnunb 4520  zrevaddclt 4592  btwnz 4613  qrevaddclt 4648  occllem5 5184

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org