Theorem ancld 305

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

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  pm5.63 353  mopick2 1479  cgsexg 1878  cgsex2g 1879  cgsex4g 1880  difsn 2518  preq12b 2537  dmcosseq 3422  relssres 3449  cores 3556  elrnopabg 3857  elunirnALT 3926  tz7.49 4017  fnoprabg 4070  omord 4257  suppsr2 5288  xrsupsslem 6158  xrinfmsslem 6159  supxrre 6165  replim 6851  cvg3i 7013  climcmplem 7227  infpn2 7601  bastop1 7731  lmfexlem1 8041  xplm 8060  bcthlem8 8091  grpidinvlem3 8135  grpinveu 8148  efifolem2 8806  pjthlem12 9313  idcnop 9988

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