Theorem imdistani 491

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  2eu1 1853  difrab 2868  dfwe2OLD 3862  onint 3876  foconst 4629  dffo4 4793  dffo5 4794  isofrlem 4878  tz7.48lem 5164  oeworde 5268  opthreg 5709  axrepndlem2 6097  axunnd 6100  axpowndlem2 6102  axpowndlem3 6103  axpowndlem4 6104  axregndlem2 6107  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116  suppsr2 6375  recgt1i 7083  sup2 7260  recnz 7403  sqrlem5 7927  iserzgt0 8472  mulc1cncf 8541  cos01gt0 8743  dscmet 9196  iscms2 9272  blocnilem 9804  efifolem4 10079  efifolem5 10080  uptx 10226  osumlem1 11213  3oalem1 11242  tolat 14631  ablcomgrp 14702  bsi 14845  taralt 15211  isfclus 15606  syldanl 15649  difxp 15690  elfzp12 15795  seqpo 15814  incsequz 15815  incsequz2 15816  fsum00 15820  fsumlt 15821  fsumlt1 15831  iccsplit 15854  oprpiece1res2 15881  lmtlm 15908  sstotbnd 15936  ismtycnv 15949  ismtyhmeo 15951  ismtybndlem 15952  heiborlem12 15966  heiborlem13 15967  heiborlem15 15969  heiborlem16 15970  heiborlem23 15977  heiborlem35 15989  heiborlem36 15990  rrndstprj2 16018  rrncms 16019  rrntotbndlem1 16020  rrntotbnd 16022  phtpycom 16050  prnc 16215  clatlat 16893

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 164  df-an 242

Copyright terms: Public domain