Theorem ancli 556

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 519	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 209  df-an 400

This theorem is referenced by:  barbariALT  2697  n0rex  4311  swopo  5567  xpdifid  6154  xpdifcnvepel  6155  xpima  6169  elrnrexdm  7071  mapex  7922  ixpsnf1o  8921  inf3lem6  9589  rankuni  9822  cardprclem  9938  nqpr  10973  letrp1  12036  p1le  12037  sup2  12149  peano2uz2  12662  uzind  12666  qreccl  12971  xrsupsslem  13311  supxrunb1  13323  faclbnd4lem4  14310  cshweqdifid  14834  fsumsplit1  15773  fprodsplit1f  16021  catcone0  17720  mndpsuppss  18800  efgred  19789  srgbinom  20282  c0mgm  20509  c0mhm  20510  lmodfopne  20968  ring2idlqus1  21390  m1detdiag  22658  1elcpmat  22776  phtpcer  25058  pntrlog2bndlem2  27643  wlkres  29870  clwwlkf  30250  hvpncan  31243  chsupsn  31617  ssjo  31651  elim2ifim  32745  rrhre  34319  pmeasadd  34623  bnj596  35043  bnj1209  35092  bnj996  35252  bnj1110  35278  bnj1189  35305  swrdrevpfx  35468  pfxwlk  35475  cusgr3cyclex  35487  satefvfmla0  35769  satefvfmla1  35776  arg-ax  36777  unirep  38214  idomnnzpownz  42750  ringexp0nn  42752  sn-sup2  43114  rp-isfinite6  44095  clsk1indlem2  44619  ntrclsss  44640  clsneiel1  44685  monoords  45877  fmul01  46157  fmuldfeqlem1  46159  fmuldfeq  46160  fmul01lt1lem1  46161  icccncfext  46462  iblspltprt  46548  stoweidlem3  46578  stoweidlem17  46592  stoweidlem19  46594  stoweidlem20  46595  stoweidlem23  46598  stirlinglem15  46663  fourierdlem16  46698  fourierdlem21  46703  fourierdlem72  46753  fourierdlem89  46770  fourierdlem90  46771  fourierdlem91  46772  hoidmvlelem4  47173  salpreimagelt  47282  salpreimalegt  47284  simpcntrab  47445  zeoALTV  48293  2zrngnmrid  48879  linc0scn0  49046  eenglngeehlnm  49362  indthinc  50084  indthincALT  50085