Theorem ancli 546

Description: Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)

Hypothesis

Ref	Expression
ancli.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ancli	⊢ (𝜑 → (𝜑 ∧ 𝜓))

Proof of Theorem ancli

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		ancli.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	jca 509	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-an 387

This theorem is referenced by:  pm4.45im  865  barbariALT  2753  cesaroOLD  2764  camestrosOLD  2766  calemosOLD  2783  n0rex  4164  swopo  5273  xpdifid  5803  xpima  5817  elrnrexdm  6612  ixpsnf1o  8215  php4  8416  ssnnfi  8448  inf3lem6  8807  rankuni  9003  cardprclem  9118  nqpr  10151  letrp1  11195  p1le  11196  sup2  11309  peano2uz2  11793  uzind  11797  uzid  11983  qreccl  12091  xrsupsslem  12425  supxrunb1  12437  faclbnd4lem4  13376  cshweqdifid  13941  fprodsplit1f  15093  idghm  18026  efgred  18514  srgbinom  18899  subrgid  19138  lmodfopne  19257  m1detdiag  20771  1elcpmat  20890  phtpcer  23164  pntrlog2bndlem2  25680  wlkres  26969  wlkresOLD  26971  clwwlkfOLD  27392  clwwlkf  27397  hvpncan  28451  chsupsn  28827  ssjo  28861  elim2ifim  29912  rrhre  30610  pmeasadd  30932  bnj596  31362  bnj1209  31413  bnj996  31571  bnj1110  31596  bnj1189  31623  arg-ax  32948  bj-mo3OLD  33356  unirep  34050  rp-isfinite6  38705  clsk1indlem2  39180  ntrclsss  39201  clsneiel1  39246  monoords  40309  fsumsplit1  40599  fmul01  40607  fmuldfeqlem1  40609  fmuldfeq  40610  fmul01lt1lem1  40611  icccncfext  40895  iblspltprt  40983  stoweidlem3  41014  stoweidlem17  41028  stoweidlem19  41030  stoweidlem20  41031  stoweidlem23  41034  stirlinglem15  41099  fourierdlem16  41134  fourierdlem21  41139  fourierdlem72  41189  fourierdlem89  41206  fourierdlem90  41207  fourierdlem91  41208  hoidmvlelem4  41606  salpreimalegt  41714  zeoALTV  42411  c0mgm  42756  c0mhm  42757  2zrngnmrid  42797  mndpsuppss  42999  linc0scn0  43059  eenglngeehlnm  43290