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 879  fvreseq 3790  oawordri 4174  omwordri 4193  oeordsuc 4211  phplem4 4497  muladdt 5401  fzaddelt 6440  fzsubelt 6441  mulexpt 6533  faclbnd5 6898  climaddlem3 7060  metreslem 7774  metxp 7786  xplm 7925  xpcn 7926  oprcn 7927  phoeqi 8462  hial2eq2t 8912  hosclt 9463  hodclt 9465  spansncv 9537  5oalem3 9541  5oalem5 9543  hoaddclt 9624  hoeq1t 9696  hoeq2t 9697  hmopst 9883  leopaddt 10003  mdsymlem5 10271

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