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  2667  n0rex  4375  swopo  5622  xpdifid  6198  xpima  6212  elrnrexdm  7121  mapex  7975  ixpsnf1o  8992  inf3lem6  9698  rankuni  9928  cardprclem  10044  nqpr  11079  letrp1  12134  p1le  12135  sup2  12247  peano2uz2  12727  uzind  12731  qreccl  13030  xrsupsslem  13365  supxrunb1  13377  faclbnd4lem4  14341  cshweqdifid  14864  fsumsplit1  15789  fprodsplit1f  16032  catcone0  17740  efgred  19785  srgbinom  20253  c0mgm  20480  c0mhm  20481  lmodfopne  20915  ring2idlqus1  21347  m1detdiag  22617  1elcpmat  22735  phtpcer  25039  pntrlog2bndlem2  27631  wlkres  29697  clwwlkf  30070  hvpncan  31062  chsupsn  31436  ssjo  31470  elim2ifim  32559  rrhre  33959  pmeasadd  34282  bnj596  34714  bnj1209  34764  bnj996  34924  bnj1110  34950  bnj1189  34977  swrdrevpfx  35076  pfxwlk  35083  cusgr3cyclex  35096  satefvfmla0  35378  satefvfmla1  35385  arg-ax  36329  unirep  37622  idomnnzpownz  42037  ringexp0nn  42039  sn-sup2  42380  rp-isfinite6  43420  clsk1indlem2  43944  ntrclsss  43965  clsneiel1  44010  monoords  45146  fmul01  45435  fmuldfeqlem1  45437  fmuldfeq  45438  fmul01lt1lem1  45439  icccncfext  45742  iblspltprt  45828  stoweidlem3  45858  stoweidlem17  45872  stoweidlem19  45874  stoweidlem20  45875  stoweidlem23  45878  stirlinglem15  45943  fourierdlem16  45978  fourierdlem21  45983  fourierdlem72  46033  fourierdlem89  46050  fourierdlem90  46051  fourierdlem91  46052  hoidmvlelem4  46453  salpreimagelt  46562  salpreimalegt  46564  simpcntrab  46725  zeoALTV  47476  2zrngnmrid  47897  mndpsuppss  48014  linc0scn0  48070  eenglngeehlnm  48391  indthinc  48637  indthincALT  48638