Theorem ancld 298

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

Hypothesis

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

Assertion

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

Proof of Theorem ancld

Step	Hyp	Ref	Expression
1		ancld.1	. 2 |- (ph -> (ps -> ch))
2		ancl 294	. 2 |- ((ps -> ch) -> (ps -> (ps /\ ch)))
3	1, 2	syl 10	1 |- (ph -> (ps -> (ps /\ ch)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm5.63 346  mopick2 1429  cgsexg 1822  cgsex2g 1823  cgsex4g 1824  difsn 2455  preq12b 2474  dmcosseq 3349  relssres 3376  cores 3485  elrnopabg 3785  elunirnALT 3854  tz7.49 3944  fnoprabg 3997  omord 4183  suppsr2 5195  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  replimt 6692  cvg3 6860  climcmplem 7073  infpn2 7452  bastop 7584  lmfexlem1 7891  xplm 7909  bcthlem8 7940  grpidinvlem3 7984  grpinveu 7998  efifolem2 8638  pjthlem12 9145  idcnop 9821

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