Theorem ancli 558

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		ancli.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	jca 521	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  barbariALT  2699  n0rex  4312  swopo  5582  xpdifid  6167  xpdifcnvepel  6168  xpima  6182  elrnrexdm  7088  mapex  7943  ixpsnf1o  8942  inf3lem6  9609  rankuni  9842  cardprclem  9981  nqpr  11016  letrp1  12076  p1le  12077  sup2  12188  peano2uz2  12702  uzind  12706  qreccl  13011  xrsupsslem  13351  supxrunb1  13363  faclbnd4lem4  14352  swrdrevpfx  14830  cshweqdifid  14883  fsumsplit1  15821  fprodsplit1f  16069  catcone0  17767  mndpsuppss  18862  efgred  19864  srgbinom  20359  c0mgm  20589  c0mhm  20590  lmodfopne  21073  ring2idlqus1  21511  m1detdiag  22806  1elcpmat  22924  phtpcer  25207  pntrlog2bndlem2  27795  wlkres  30078  pfxwlk  30095  clwwlkf  30467  hvpncan  31464  chsupsn  31838  ssjo  31872  elim2ifim  32964  rrhre  34477  pmeasadd  34782  bnj596  35202  bnj1209  35251  bnj996  35411  bnj1110  35437  bnj1189  35464  cusgr3cyclex  35671  satefvfmla0  35949  satefvfmla1  35956  arg-ax  36986  unirep  38425  idomnnzpownz  42959  ringexp0nn  42961  sn-sup2  43325  rp-isfinite6  44304  clsk1indlem2  44828  ntrclsss  44849  clsneiel1  44894  monoords  46076  fmul01  46356  fmuldfeqlem1  46358  fmuldfeq  46359  fmul01lt1lem1  46360  icccncfext  46661  iblspltprt  46747  stoweidlem3  46777  stoweidlem17  46791  stoweidlem19  46793  stoweidlem20  46794  stoweidlem23  46797  stirlinglem15  46862  fourierdlem16  46897  fourierdlem21  46902  fourierdlem72  46952  fourierdlem89  46969  fourierdlem90  46970  fourierdlem91  46971  hoidmvlelem4  47372  salpreimagelt  47481  salpreimalegt  47483  simpcntrab  47644  zeoALTV  48495  2zrngnmrid  49080  linc0scn0  49262  eenglngeehlnm  49578  indthinc  50299  indthincALT  50300