Theorem ancli 557

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  barbariALT  2703  n0rex  4320  swopo  5581  xpdifid  6166  xpdifcnvepel  6167  xpima  6181  elrnrexdm  7085  mapex  7937  ixpsnf1o  8936  inf3lem6  9602  rankuni  9835  cardprclem  9965  nqpr  10999  letrp1  12059  p1le  12060  sup2  12171  peano2uz2  12684  uzind  12688  qreccl  12993  xrsupsslem  13333  supxrunb1  13345  faclbnd4lem4  14332  cshweqdifid  14857  fsumsplit1  15796  fprodsplit1f  16044  catcone0  17743  mndpsuppss  18823  efgred  19818  srgbinom  20313  c0mgm  20541  c0mhm  20542  lmodfopne  20999  ring2idlqus1  21430  m1detdiag  22723  1elcpmat  22841  phtpcer  25123  pntrlog2bndlem2  27708  wlkres  29959  clwwlkf  30339  hvpncan  31332  chsupsn  31706  ssjo  31740  elim2ifim  32832  rrhre  34356  pmeasadd  34660  bnj596  35080  bnj1209  35129  bnj996  35289  bnj1110  35315  bnj1189  35342  swrdrevpfx  35541  pfxwlk  35549  cusgr3cyclex  35561  satefvfmla0  35843  satefvfmla1  35850  arg-ax  36850  unirep  38287  idomnnzpownz  42823  ringexp0nn  42825  sn-sup2  43189  rp-isfinite6  44170  clsk1indlem2  44694  ntrclsss  44715  clsneiel1  44760  monoords  45942  fmul01  46222  fmuldfeqlem1  46224  fmuldfeq  46225  fmul01lt1lem1  46226  icccncfext  46527  iblspltprt  46613  stoweidlem3  46643  stoweidlem17  46657  stoweidlem19  46659  stoweidlem20  46660  stoweidlem23  46663  stirlinglem15  46728  fourierdlem16  46763  fourierdlem21  46768  fourierdlem72  46818  fourierdlem89  46835  fourierdlem90  46836  fourierdlem91  46837  hoidmvlelem4  47238  salpreimagelt  47347  salpreimalegt  47349  simpcntrab  47510  zeoALTV  48358  2zrngnmrid  48944  linc0scn0  49122  eenglngeehlnm  49438  indthinc  50159  indthincALT  50160