Theorem ancli 552

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 515	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  barbariALT  2732  n0rex  4268  swopo  5448  xpdifid  5992  xpima  6006  elrnrexdm  6832  ixpsnf1o  8485  inf3lem6  9080  rankuni  9276  cardprclem  9392  nqpr  10425  letrp1  11473  p1le  11474  sup2  11584  peano2uz2  12058  uzind  12062  uzid  12246  qreccl  12356  xrsupsslem  12688  supxrunb1  12700  faclbnd4lem4  13652  cshweqdifid  14173  fprodsplit1f  15336  efgred  18866  srgbinom  19288  lmodfopne  19665  m1detdiag  21202  1elcpmat  21320  phtpcer  23600  pntrlog2bndlem2  26162  wlkres  27460  clwwlkf  27832  hvpncan  28822  chsupsn  29196  ssjo  29230  elim2ifim  30312  rrhre  31372  pmeasadd  31693  bnj596  32127  bnj1209  32178  bnj996  32338  bnj1110  32364  bnj1189  32391  swrdrevpfx  32476  pfxwlk  32483  cusgr3cyclex  32496  satefvfmla0  32778  satefvfmla1  32785  arg-ax  33877  unirep  35151  sn-sup2  39594  rp-isfinite6  40226  clsk1indlem2  40745  ntrclsss  40766  clsneiel1  40811  monoords  41929  fsumsplit1  42214  fmul01  42222  fmuldfeqlem1  42224  fmuldfeq  42225  fmul01lt1lem1  42226  icccncfext  42529  iblspltprt  42615  stoweidlem3  42645  stoweidlem17  42659  stoweidlem19  42661  stoweidlem20  42662  stoweidlem23  42665  stirlinglem15  42730  fourierdlem16  42765  fourierdlem21  42770  fourierdlem72  42820  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  hoidmvlelem4  43237  salpreimagelt  43343  salpreimalegt  43345  simpcntrab  43484  zeoALTV  44188  c0mgm  44533  c0mhm  44534  2zrngnmrid  44574  mndpsuppss  44773  linc0scn0  44832  eenglngeehlnm  45153