Theorem anandis 515

Description: Inference that undistributes conjunction in the antecedent.

Hypothesis

Ref	Expression
anandis.1	⊢ (((φ ⋀ ψ) ⋀ (φ ⋀ χ)) → τ)

Assertion

Ref	Expression
anandis	⊢ ((φ ⋀ (ψ ⋀ χ)) → τ)

Proof of Theorem anandis

Step	Hyp	Ref	Expression
1		anandis.1	. . 3 ⊢ (((φ ⋀ ψ) ⋀ (φ ⋀ χ)) → τ)
2	1	an4s 511	. 2 ⊢ (((φ ⋀ φ) ⋀ (ψ ⋀ χ)) → τ)
3	2	anabsan 507	1 ⊢ ((φ ⋀ (ψ ⋀ χ)) → τ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  3impdi 884  sotrieq 2877  xpexr2 3496  f1fv 3890  isocnv 3912  isotr 3913  isotrALT 3914  f1oiso 3920  oaword 4199  omord2 4214  omword 4217  oeord 4231  oeword 4233  zorn2lem6 4810  ltapi 5050  ltmpi 5051  distrlem1pr 5147  distrlem4pr 5150  distrlem5pr 5151  prlem934b 5158  ltapr 5171  pre-axltadd 5309  pnpcan 5498  qbtwnre 6280  cau5ii 6949  cau5i 6951  faclbnd 6977  iserzcmp0i 7175  fsum0diaglem2 7289  infxpidmlem1 7585  tgcl 7654  uncld 7707  innei 7762  cnco 7794  metreslem 7848  metcnpi3 7918  metcnpi4 7919  metcni2 7921  iscau5 7967  iscaunns 7970  caussi 7980  causs 7981  bcthlem21 8045  grpinvf 8104  vcsub4 8220  nvaddsub4 8306  nvcni3 8356  lnosub 8445  minveclem27 8596  minveclem28 8597  hcau2 9079  ocorth 9188  projlem28 9237  fh1 9585  fh2 9586  spansncvi 9621  unopf1o 9864  counop 9869  lnopmi 9949  adjlnop 10043

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