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 494  mo 1395  2mo 1450  disjsn 2445  oelim2 4228  php4 4523  ssnnfi 4545  ssnnfiOLD 4546  inf3lem6 4627  rankuni 4708  1idpr 5145  prlem934 5151  divdivdivt 5787  letrp1t 5818  p1let 5819  sup2 6053  xrsupsslem 6078  supxrunb1 6091  zltp1let 6183  peano2uz2 6203  uzind 6207  flget 6235  fladdzt 6246  qrecclt 6274  uzidt 6428  seqz1 6548  seq1ublem 6911  faclbnd4lem4 6951  fsumsplit 7020  fsumrev2 7030  abscncflem 7274  infpss 7575  xplmi 7970  sqcn 8331  hvpncant 8903  chsupsn 9307  nlelch 9989

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