Theorem anandis 512

Description: Inference that undistributes conjunction in the antecedent.

Hypothesis

Ref	Expression
anandis.1	|- (((ph /\ ps) /\ (ph /\ ch)) -> ta)

Assertion

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

Proof of Theorem anandis

Step	Hyp	Ref	Expression
1		anandis.1	. . 3 |- (((ph /\ ps) /\ (ph /\ ch)) -> ta)
2	1	an4s 508	. 2 |- (((ph /\ ph) /\ (ps /\ ch)) -> ta)
3	2	anabsan 504	1 |- ((ph /\ (ps /\ ch)) -> ta)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  3impdi 878  sotrieq 2856  xpexr2 3472  f1fv 3865  isocnv 3887  isotr 3888  isotrALT 3889  f1oiso 3895  oaword 4173  omord2 4188  omword 4191  oeord 4205  oeword 4207  zorn2lem6 4773  ltapi 5010  ltmpi 5011  distrlem1pr 5107  distrlem4pr 5110  distrlem5pr 5111  prlem934b 5118  ltapr 5131  pre-axltadd 5269  pnpcant 5458  qbtwnre 6224  cau5i 6862  cau5 6864  faclbnd 6890  iserzcmp0 7087  fsum0diaglem2 7200  infxpidmlem1 7503  tgclt 7574  uncld 7631  innei 7686  cnco 7718  metreslem 7774  metcnpi3 7844  metcnpi4 7845  metcni2 7847  iscau5 7893  caussi 7905  causs 7906  bcthlem21 7969  grpinvf 8029  vcsub4 8147  nvaddsub4 8233  lnosub 8366  minveclem27 8515  minveclem28 8516  hcau2 8994  ocorth 9103  projlem28 9152  fh1t 9501  fh2t 9502  spansncv 9537  unopf1ot 9779  counopt 9784  lnopm 9863  adjlnopt 9957

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