Theorem imdistani 340

Description: Distribution of implication with conjunction.

Hypothesis

Ref	Expression
imdistani.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
imdistani	|- ((ph /\ ps) -> (ph /\ ch))

Proof of Theorem imdistani

Step	Hyp	Ref	Expression
1		imdistani.1	. . 3 |- (ph -> (ps -> ch))
2	1	anc2li 250	. 2 |- (ph -> (ps -> (ph /\ ch)))
3	2	imp 277	1 |- ((ph /\ ps) -> (ph /\ ch))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  2eu1 1067  difrab 1695  dfwe2 2187  onint 2261  isofrlem 2939  tz7.48lem 2993  opthreg 3455  axrepndlem2 3739  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  suppsr2 4017  sup2 4510  sqrlem5 4735  osumlem1 5530  3oalem1 5552

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