Theorem imdistani 443

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 302	. 2 |- (ph -> (ps -> (ph /\ ch)))
3	2	imp 350	1 |- ((ph /\ ps) -> (ph /\ ch))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  2eu1 1447  difrab 2269  dfwe2 2930  onint 3001  foconst 3674  dffo4 3811  dffo5 3812  isofrlem 3892  tz7.48lem 3946  oeworde 4210  opthreg 4584  axrepndlem2 4925  axunnd 4928  axpowndlem2 4930  axpowndlem3 4931  axpowndlem4 4932  axregndlem2 4935  axinfndlem1 4937  axinfnd 4938  axacndlem4 4942  axacndlem5 4943  axacnd 4944  suppsr2 5203  recgt1it 5856  sup2 6006  recnzt 6146  sqrlem5 6615  ser1f0 7114  iserzgt0 7154  mulc1cncf 7222  cos01gt0 7427  dscmet 7870  iscms2 7944  blocnilem 8408  efifolem4 8659  efifolem5 8660  osumlem1 9518  3oalem1 9547  bsi 10418

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