Theorem anandis 514

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 510	. 2 |- (((ph /\ ph) /\ (ps /\ ch)) -> ta)
3	2	anabsan 506	1 |- ((ph /\ (ps /\ ch)) -> ta)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  3impdi 882  sotrieq 2867  xpexr2 3486  f1fv 3880  isocnv 3902  isotr 3903  isotrALT 3904  f1oiso 3910  oaword 4189  omord2 4204  omword 4207  oeord 4221  oeword 4223  zorn2lem6 4803  ltapi 5042  ltmpi 5043  distrlem1pr 5139  distrlem4pr 5142  distrlem5pr 5143  prlem934b 5150  ltapr 5163  pre-axltadd 5301  pnpcant 5490  qbtwnre 6279  cau5i 6917  cau5 6919  faclbnd 6945  iserzcmp0 7143  fsum0diaglem2 7257  infxpidmlem1 7553  tgclt 7623  uncld 7678  innei 7733  cnco 7765  metreslem 7819  metcnpi3 7889  metcnpi4 7890  metcni2 7892  iscau5 7938  iscaunns 7941  caussi 7951  causs 7952  bcthlem21 8016  grpinvf 8075  vcsub4 8191  nvaddsub4 8277  nvcni3 8327  lnosub 8416  minveclem27 8567  minveclem28 8568  hcau2 9050  ocorth 9159  projlem28 9208  fh1t 9556  fh2t 9557  spansncv 9592  unopf1ot 9835  counopt 9840  lnopm 9920  adjlnopt 10014

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