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 1442  reupick 2269  prel12 2475  dfwe2 2925  ordpwsuc 3056  ordunisuc2 3105  dfom2 3123  nnsuc 3138  ssrnres 3467  funssres 3538  dffo4 3805  dffo5 3806  ltexpq2 5053  ltexpri 5121  suplem1pr 5133  lbinfm 5995  replimt 6692  cau4i 6855  cau5 6856  cvg3 6860  infcvglem3 7158  xplm 7909  minveclem27 8502  atexcht 10216

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