Theorem ancli 296

Description: Deduction conjoining antecedent to left of consequent.

Hypothesis

Ref	Expression
ancli.1	|- (ph -> ps)

Assertion

Ref	Expression
ancli	|- (ph -> (ph /\ ps))

Proof of Theorem ancli

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ph -> ph)
2		ancli.1	. 2 |- (ph -> ps)
3	1, 2	jca 288	1 |- (ph -> (ph /\ ps))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  pm4.45im 332  anabs1 491  mo 1386  2mo 1440  disjsn 2431  oelim2 4206  php4 4496  ssnn 4514  inf3lem6 4590  rankuni 4670  1idpr 5105  prlem934 5111  divdivdivt 5741  letrp1t 5772  p1let 5773  sup2 5998  xrsupsslem 6023  supxrunb1 6036  zltp1let 6128  peano2uz2 6149  uzind 6153  flget 6178  fladdzt 6187  qrecclt 6211  uzidt 6359  seqz1 6479  seq1ublem 6848  faclbnd4lem4 6888  fsumsplit 6958  fsumrev2 6968  abscncflem 7209  xplmi 7907  sqcn 8270  hvpncant 8829  chsupsn 9227  nlelch 9909

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