Theorem ancli 296

Description: Deduction conjoining antecedent to left of consequent.

Hypothesis

Ref	Expression
ancli.1	⊢ (φ → ψ)

Assertion

Ref	Expression
ancli	⊢ (φ → (φ ⋀ ψ))

Proof of Theorem ancli

Step	Hyp	Ref	Expression
1		id 59	. 2 ⊢ (φ → φ)
2		ancli.1	. 2 ⊢ (φ → ψ)
3	1, 2	jca 288	1 ⊢ (φ → (φ ⋀ ψ))

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  pm4.45im 332  anabs1 495  mo 1399  2mo 1454  disjsn 2451  oelim2 4236  php4 4531  ssnnfi 4550  inf3lem6 4630  rankuni 4710  1idpr 5146  prlem934 5152  divdivdivt 5789  letrp1t 5820  p1let 5821  sup2 6057  xrsupsslem 6082  supxrunb1 6095  zltp1let 6187  peano2uz2 6210  uzind 6214  flget 6242  fladdzt 6253  qrecclt 6283  uzidt 6377  seqz1 6560  seq1ublem 6925  faclbnd4lem4 6965  fsumsplit 7034  fsumrev2 7044  abscncflem 7288  infpss 7589  xplmi 7982  sqcn 8343  hvpncant 8915  chsupsn 9319  nlelch 10001

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