Theorem anandis 873

Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)

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

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  3impdi  1381  dff13  6512  f1oiso  6601  omord2  7647  fodomacn  8879  ltapi  9725  ltmpi  9726  axpre-ltadd  9988  faclbnd  13077  pwsdiagmhm  17369  tgcl  20773  brbtwn2  25785  grpoinvf  27386  ocorth  28150  fh1  28477  fh2  28478  spansncvi  28511  lnopmi  28859  adjlnop  28945  matunitlindflem2  33406  poimirlem4  33413  heicant  33444  mblfinlem2  33447  ismblfin  33450  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anc  33493