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 1447  reupick 2275  prel12 2480  dfwe2 2930  ordpwsuc 3061  ordunisuc2 3110  dfom2 3128  nnsuc 3143  ssrnres 3473  funssres 3544  dffo4 3811  dffo5 3812  ltexpq2 5061  ltexpri 5129  suplem1pr 5141  lbinfm 6003  replimt 6700  cau4i 6863  cau5 6864  cvg3 6868  infcvglem3 7166  xplm 7925  minveclem27 8515  atexcht 10245

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