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 1442  difrab 2263  dfwe2 2925  onint 2996  foconst 3668  dffo4 3805  dffo5 3806  isofrlem 3886  tz7.48lem 3940  oeworde 4204  opthreg 4576  axrepndlem2 4917  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axregndlem2 4927  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  suppsr2 5195  recgt1it 5848  sup2 5998  recnzt 6138  sqrlem5 6607  ser1f0 7106  iserzgt0 7146  mulc1cncf 7214  cos01gt0 7419  dscmet 7856  iscms2 7928  blocnilem 8395  efifolem4 8640  efifolem5 8641  osumlem1 9495  3oalem1 9524  bsi 10382

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