Theorem ancli 294

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 286	1 |- (ph -> (ph /\ ps))

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  pm4.45im 330  anabs1 495  mo 1432  2mo 1487  disjsn 2502  oelim2 4358  php4 4663  ssnnfi 4682  inf3lem6 4763  rankuni 4844  1idpr 5287  prlem934 5293  letrp1 5956  p1le 5957  sup2 6219  xrsupsslem 6244  supxrunb1 6257  zltp1le 6349  peano2uz2 6372  uzind 6376  qreccl 6412  flge 6431  fladdz 6443  uzid 6554  seqz1 6742  seq1ublem 7114  faclbnd4lem4 7154  fsumsplit 7223  fsumrev2 7233  abscncflem 7479  infpss 7786  xplmi 8184  grpidval 8275  sqcn 8589  hvpncan 9183  chsupsn 9588  nlelchi 10273  fgfil 11638  tailf 11756

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 145  df-an 223

Copyright terms: Public domain