Theorem ancrd 306

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 302	. 2 |- ((ps -> ch) -> (ps -> (ch /\ ps)))
3	1, 2	syl 10	1 |- (ph -> (ps -> (ch /\ ps)))

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  impac 396  2eu1 1492  reupick 2330  prel12 2538  dfwe2 2992  ordpwsuc 3123  ordunisuc2 3172  dfom2 3190  nnsuc 3205  ssrnres 3538  funssres 3609  dffo4 3877  dffo5 3878  ltexpq2 5146  ltexpri 5214  suplem1pr 5226  lbinfm 6130  replim 6851  cau4ii 7008  cau5i 7009  cvg3i 7013  infcvglem3 7313  xplm 8060  minveclem27 8655  atexch 10392  iepiclem 10833

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 154  df-an 232

Copyright terms: Public domain