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 1448  difrab 2270  dfwe2 2931  onint 3002  foconst 3678  dffo4 3815  dffo5 3816  isofrlem 3896  tz7.48lem 3950  oeworde 4213  opthreg 4587  axrepndlem2 4928  axunnd 4931  axpowndlem2 4933  axpowndlem3 4934  axpowndlem4 4935  axregndlem2 4938  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947  suppsr2 5206  recgt1it 5858  sup2 6008  recnzt 6148  sqrlem5 6622  ser1f0 7123  iserzgt0 7163  mulc1cncf 7231  cos01gt0 7436  dscmet 7880  iscms2 7956  blocnilem 8423  efifolem4 8675  efifolem5 8676  osumlem1 9535  3oalem1 9564  bsi 10441

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