Theorem ancrd 297

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

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  impac 387  2eu1 1489  reupick 2331  prel12 2549  dfwe2 3140  ordpwsuc 3172  ordunisuc2 3198  dfom2 3220  nnsuc 3235  ssrnres 3566  funssres 3657  dffo4 3934  dffo5 3935  ltexpq2 5235  ltexpri 5303  suplem1pr 5315  lbinfm 6216  replim 6962  cau4ii 7121  cau5i 7122  cvg3i 7126  infcvglem3 7427  xplm 8186  minveclem27 8831  atexch 10590  iepiclem 11278  ordiso 11426  onsdom 11437  extbas1 11641  filnet 11768

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 145  df-an 223

Copyright terms: Public domain