Theorem ancri 245

Description: Deduction conjoining antecedent to right of consequent.

Hypothesis

Ref	Expression
ancri.1	⊢ (φ → ψ)

Assertion

Ref	Expression
ancri	⊢ (φ → (ψ ∧ φ))

Proof of Theorem ancri

Step	Hyp	Ref	Expression
1		ancri.1	. 2 ⊢ (φ → ψ)
2		id 9	. 2 ⊢ (φ → φ)
3	1, 2	jca 236	1 ⊢ (φ → (ψ ∧ φ))

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