Theorem ancli 244

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 9	. 2 |- (ph -> ph)
2		ancli.1	. 2 |- (ph -> ps)
3	1, 2	jca 236	1 |- (ph -> (ph /\ ps))

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  pm4.45im 267  mo 1020  disjsn 1836  fnoprab 3038  php4 3412  ssnn 3429  inf3lem6 3469  1idpr 3927  prlem934 3933  mulcmpblnr 3977  divdivdivt 4265  sup2 4510  zltp1let 4597  peano2uz 4602  flgzt 4626  qrecclt 4646  hvsubcan1t 5016  chsupsn 5313

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