Theorem ancli 548

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  barbariALT  2670  n0rex  4297  swopo  5550  xpdifid  6132  xpima  6146  elrnrexdm  7041  mapex  7892  ixpsnf1o  8886  inf3lem6  9554  rankuni  9787  cardprclem  9903  nqpr  10937  letrp1  11999  p1le  12000  sup2  12112  peano2uz2  12617  uzind  12621  qreccl  12919  xrsupsslem  13259  supxrunb1  13271  faclbnd4lem4  14258  cshweqdifid  14782  fsumsplit1  15707  fprodsplit1f  15955  catcone0  17653  mndpsuppss  18733  efgred  19723  srgbinom  20212  c0mgm  20439  c0mhm  20440  lmodfopne  20895  ring2idlqus1  21317  m1detdiag  22562  1elcpmat  22680  phtpcer  24962  pntrlog2bndlem2  27541  wlkres  29737  clwwlkf  30117  hvpncan  31110  chsupsn  31484  ssjo  31518  elim2ifim  32615  rrhre  34165  pmeasadd  34469  bnj596  34889  bnj1209  34938  bnj996  35098  bnj1110  35124  bnj1189  35151  swrdrevpfx  35299  pfxwlk  35306  cusgr3cyclex  35318  satefvfmla0  35600  satefvfmla1  35607  arg-ax  36598  unirep  38035  idomnnzpownz  42571  ringexp0nn  42573  sn-sup2  42936  rp-isfinite6  43945  clsk1indlem2  44469  ntrclsss  44490  clsneiel1  44535  monoords  45730  fmul01  46010  fmuldfeqlem1  46012  fmuldfeq  46013  fmul01lt1lem1  46014  icccncfext  46315  iblspltprt  46401  stoweidlem3  46431  stoweidlem17  46445  stoweidlem19  46447  stoweidlem20  46448  stoweidlem23  46451  stirlinglem15  46516  fourierdlem16  46551  fourierdlem21  46556  fourierdlem72  46606  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  hoidmvlelem4  47026  salpreimagelt  47135  salpreimalegt  47137  simpcntrab  47298  zeoALTV  48146  2zrngnmrid  48732  linc0scn0  48899  eenglngeehlnm  49215  indthinc  49937  indthincALT  49938