Theorem anandirs 513

Description: Inference that undistributes conjunction in the antecedent.

Hypothesis

Ref	Expression
anandirs.1	|- (((ph /\ ch) /\ (ps /\ ch)) -> ta)

Assertion

Ref	Expression
anandirs	|- (((ph /\ ps) /\ ch) -> ta)

Proof of Theorem anandirs

Step	Hyp	Ref	Expression
1		anandirs.1	. . 3 |- (((ph /\ ch) /\ (ps /\ ch)) -> ta)
2	1	an4s 508	. 2 |- (((ph /\ ps) /\ (ch /\ ch)) -> ta)
3	2	anabsan2 505	1 |- (((ph /\ ps) /\ ch) -> ta)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  3impdir 881  fvreseq 3799  oawordri 4184  omwordri 4203  oeordsuc 4221  phplem4 4511  muladdt 5421  fzaddelt 6500  fzsubelt 6501  mulexpt 6594  faclbnd5 6953  climaddlem3 7116  metreslem 7822  metxp 7834  xplm 7975  xpcn 7976  oprcn 7977  phoeqi 8518  hial2eq2t 8973  hosclt 9523  hodclt 9525  spansncv 9597  5oalem3 9601  5oalem5 9603  hoaddclt 9684  hoeq1t 9756  hoeq2t 9757  hmopst 9945  leopaddt 10065  mdsymlem5 10334

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