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 880  sotrieq 2861  xpexr2 3480  f1fv 3874  isocnv 3896  isotr 3897  isotrALT 3898  f1oiso 3904  oaword 4183  omord2 4198  omword 4201  oeord 4215  oeword 4217  zorn2lem6 4793  ltapi 5030  ltmpi 5031  distrlem1pr 5127  distrlem4pr 5130  distrlem5pr 5131  prlem934b 5138  ltapr 5151  pre-axltadd 5289  pnpcant 5478  qbtwnre 6278  cau5i 6917  cau5 6919  faclbnd 6945  iserzcmp0 7143  fsum0diaglem2 7257  infxpidmlem1 7552  tgclt 7624  uncld 7681  innei 7736  cnco 7768  metreslem 7822  metcnpi3 7892  metcnpi4 7893  metcni2 7895  iscau5 7941  iscaunns 7944  caussi 7954  causs 7955  bcthlem21 8019  grpinvf 8079  vcsub4 8195  nvaddsub4 8281  nvcni3 8331  lnosub 8420  minveclem27 8571  minveclem28 8572  hcau2 9055  ocorth 9164  projlem28 9213  fh1t 9561  fh2t 9562  spansncv 9597  unopf1ot 9840  counopt 9845  lnopm 9925  adjlnopt 10019

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