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 496  orabs 583  fo00 3721  tz7.48lem 3961  tz7.48-1 3962  caoprmo 4076  oewordri 4225  zfregs 4657  ltexprlem4 5157  recexpr 5172  suplem2pr 5174  recexsrlem 5224  xrinfmsslem 6079  flget 6235  fladdzt 6246  qrecclt 6274  bccl2t 6971  infxpidmlem11 7563  minveclem24 8564  fiv 10470

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