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 580  fo00 3706  tz7.48lem 3946  tz7.48-1 3947  caoprmo 4062  oewordri 4209  zfregs 4627  ltexprlem4 5125  recexpr 5140  suplem2pr 5142  recexsrlem 5192  xrinfmsslem 6032  flget 6186  fladdzt 6195  qrecclt 6219  bccl2t 6917  infxpidmlem11 7513  minveclem24 8512  fiv 10410

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