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  2697  n0rex  4312  swopo  5580  xpdifid  6165  xpdifcnvepel  6166  xpima  6180  elrnrexdm  7084  mapex  7933  ixpsnf1o  8932  inf3lem6  9598  rankuni  9831  cardprclem  9961  nqpr  10994  letrp1  12054  p1le  12055  sup2  12166  peano2uz2  12679  uzind  12683  qreccl  12988  xrsupsslem  13328  supxrunb1  13340  faclbnd4lem4  14328  cshweqdifid  14853  fsumsplit1  15792  fprodsplit1f  16040  catcone0  17738  mndpsuppss  18818  efgred  19813  srgbinom  20308  c0mgm  20537  c0mhm  20538  lmodfopne  21021  ring2idlqus1  21459  m1detdiag  22754  1elcpmat  22872  phtpcer  25154  pntrlog2bndlem2  27742  wlkres  30018  clwwlkf  30398  hvpncan  31391  chsupsn  31765  ssjo  31799  elim2ifim  32891  rrhre  34411  pmeasadd  34715  bnj596  35135  bnj1209  35184  bnj996  35344  bnj1110  35370  bnj1189  35397  swrdrevpfx  35608  pfxwlk  35616  cusgr3cyclex  35628  satefvfmla0  35910  satefvfmla1  35917  arg-ax  36947  unirep  38385  idomnnzpownz  42919  ringexp0nn  42921  sn-sup2  43285  rp-isfinite6  44264  clsk1indlem2  44788  ntrclsss  44809  clsneiel1  44854  monoords  46036  fmul01  46316  fmuldfeqlem1  46318  fmuldfeq  46319  fmul01lt1lem1  46320  icccncfext  46621  iblspltprt  46707  stoweidlem3  46737  stoweidlem17  46751  stoweidlem19  46753  stoweidlem20  46754  stoweidlem23  46757  stirlinglem15  46822  fourierdlem16  46857  fourierdlem21  46862  fourierdlem72  46912  fourierdlem89  46929  fourierdlem90  46930  fourierdlem91  46931  hoidmvlelem4  47332  salpreimagelt  47441  salpreimalegt  47443  simpcntrab  47604  zeoALTV  48455  2zrngnmrid  49041  linc0scn0  49223  eenglngeehlnm  49539  indthinc  50260  indthincALT  50261