Theorem ancrd 299

Description: Deduction conjoining antecedent to right of consequent in nested implication.

Hypothesis

Ref	Expression
ancrd.1	|- (ph -> (ps -> ch))

Assertion

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

Proof of Theorem ancrd

Step	Hyp	Ref	Expression
1		ancrd.1	. 2 |- (ph -> (ps -> ch))
2		ancr 295	. 2 |- ((ps -> ch) -> (ps -> (ch /\ ps)))
3	1, 2	syl 10	1 |- (ph -> (ps -> (ch /\ ps)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  impac 387  2eu1 1449  reupick 2279  prel12 2484  dfwe2 2935  ordpwsuc 3066  ordunisuc2 3115  dfom2 3133  nnsuc 3148  ssrnres 3481  funssres 3552  dffo4 3820  dffo5 3821  ltexpq2 5081  ltexpri 5149  suplem1pr 5161  lbinfm 6048  replimt 6761  cau4i 6918  cau5 6919  cvg3 6923  infcvglem3 7223  xplm 7975  minveclem27 8571  atexcht 10308

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