Theorem anandis 570

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  3impdi 1152  sotrieqOLD 3617  xpexr2 4353  dff13 4850  isocnv 4873  isotr 4874  isotrALT 4875  f1oiso 4881  oawordOLD 5231  omord2 5246  omword 5249  oeord 5263  oeword 5265  zorn2lem6 5955  ltapi 6182  ltmpi 6183  distrlem1pr 6279  distrlem4pr 6282  distrlem5pr 6283  prlem934b 6290  ltapr 6303  pre-axltadd 6442  pnpcan 6645  qbtwnre 7459  cau5ii 8169  cau5i 8171  faclbnd 8197  iserzcmp0 8403  fsum0diaglem2 8519  infxpidmlem1 8821  tgcl 8894  uncld 8957  innei 9012  cnco 9045  metreslem 9099  metcnpi3 9170  metcnpi4 9171  metcni2 9173  iscau5 9219  iscaunns 9222  caussi 9232  causs 9233  bcthlem21 9297  grpinvf 9364  vcsub4 9527  nvaddsub4 9613  nvcni3 9663  lnosub 9759  minveclem27 9916  minveclem28 9917  hcau2 10688  ocorth 10797  projlem28 10846  fh1 11194  fh2 11195  spansncvi 11232  unopf1o 11477  counop 11482  lnopmi 11562  adjlnop 11656  mulgcdlem2 13757

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