Theorem ancri 245

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

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  oel 441  tz7.48lem 2993  tz7.48-1 2994  caoprmo 3084  zfregs 3491  ltexprlem4 3939  recexpr 3954  suplem2pr 3956  recexsrlem 4006  flgzt 4626  qrecclt 4646  infxpidmlem11 4943

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org