Theorem ancri 321

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 73	. 2 |- (ph -> ph)
3	1, 2	jca 310	1 |- (ph -> (ps /\ ph))

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  anabs7 552  orabs 641  gencbvex 2334  trsuc 3752  fo00 4669  caoprmo 5003  tz7.48lem 5164  tz7.48-1 5165  oewordri 5267  zfregs 5754  ltexprlem4 6297  recexpr 6312  suplem2pr 6314  recexsrlem 6364  xrinfmsslem 7286  flge 7472  fladdz 7484  bccl2 8223  infxpidmlem11 8831  minveclem24 9913  fiv 10212  ismnd2 10392  bnj512 12519  bnj542 12536  bnj851 12786  trcrm 14286  ref4w 14370  is2ndc2 15473  eqfnoprv2 15704  lincmb01icc 15879  heiborlem17 15971  reparphtlem2 16064  reparpht 16065  iotasbc 16383

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 164  df-an 242

Copyright terms: Public domain