Theorem anandis 804

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  3impdi  1239  dff13  5971  f1oiso  6038  omord2  6777  fodomacn  7901  ltapi  8744  ltmpi  8745  axpre-ltadd  9006  faclbnd  11544  pwsdiagmhm  14731  tgcl  16997  grpoinvf  21789  ocorth  22754  fh1  23081  fh2  23082  spansncvi  23115  lnopmi  23464  adjlnop  23550  brbtwn2  25756  mblfinlem  26151  ismblfin  26154

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

This theorem depends on definitions:  df-bi 178  df-an 361