Theorem ancri 297

Description: Deduction conjoining antecedent to right of consequent.

Hypothesis

Ref	Expression
ancri.1	|- (ph -> ps)

Assertion

Ref	Expression
ancri	|- (ph -> (ps /\ ph))

Proof of Theorem ancri

Step	Hyp	Ref	Expression
1		ancri.1	. 2 |- (ph -> ps)
2		id 59	. 2 |- (ph -> ph)
3	1, 2	jca 288	1 |- (ph -> (ps /\ ph))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anabs7 494  orabs 581  fo00 3715  tz7.48lem 3955  tz7.48-1 3956  caoprmo 4070  oewordri 4219  zfregs 4647  ltexprlem4 5145  recexpr 5160  suplem2pr 5162  recexsrlem 5212  xrinfmsslem 6077  flget 6233  fladdzt 6244  qrecclt 6273  bccl2t 6971  infxpidmlem11 7562  minveclem24 8568  fiv 10482  fivOLD 10483

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