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  2668  n0rex  4339  swopo  5585  xpdifid  6170  xpima  6184  elrnrexdm  7090  mapex  7946  ixpsnf1o  8961  inf3lem6  9656  rankuni  9886  cardprclem  10002  nqpr  11037  letrp1  12094  p1le  12095  sup2  12207  peano2uz2  12690  uzind  12694  qreccl  12994  xrsupsslem  13332  supxrunb1  13344  faclbnd4lem4  14318  cshweqdifid  14841  fsumsplit1  15764  fprodsplit1f  16009  catcone0  17706  mndpsuppss  18752  efgred  19739  srgbinom  20201  c0mgm  20432  c0mhm  20433  lmodfopne  20871  ring2idlqus1  21296  m1detdiag  22570  1elcpmat  22688  phtpcer  24982  pntrlog2bndlem2  27577  wlkres  29635  clwwlkf  30013  hvpncan  31005  chsupsn  31379  ssjo  31413  elim2ifim  32505  rrhre  33963  pmeasadd  34268  bnj596  34701  bnj1209  34751  bnj996  34911  bnj1110  34937  bnj1189  34964  swrdrevpfx  35063  pfxwlk  35070  cusgr3cyclex  35082  satefvfmla0  35364  satefvfmla1  35371  arg-ax  36358  unirep  37662  idomnnzpownz  42074  ringexp0nn  42076  sn-sup2  42446  rp-isfinite6  43476  clsk1indlem2  44000  ntrclsss  44021  clsneiel1  44066  monoords  45254  fmul01  45540  fmuldfeqlem1  45542  fmuldfeq  45543  fmul01lt1lem1  45544  icccncfext  45847  iblspltprt  45933  stoweidlem3  45963  stoweidlem17  45977  stoweidlem19  45979  stoweidlem20  45980  stoweidlem23  45983  stirlinglem15  46048  fourierdlem16  46083  fourierdlem21  46088  fourierdlem72  46138  fourierdlem89  46155  fourierdlem90  46156  fourierdlem91  46157  hoidmvlelem4  46558  salpreimagelt  46667  salpreimalegt  46669  simpcntrab  46830  zeoALTV  47603  2zrngnmrid  48118  linc0scn0  48286  eenglngeehlnm  48606  indthinc  49075  indthincALT  49076