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  2673  n0rex  4380  swopo  5619  xpdifid  6201  xpima  6215  elrnrexdm  7125  mapex  7981  ixpsnf1o  8998  inf3lem6  9704  rankuni  9934  cardprclem  10050  nqpr  11085  letrp1  12140  p1le  12141  sup2  12253  peano2uz2  12733  uzind  12737  qreccl  13036  xrsupsslem  13371  supxrunb1  13383  faclbnd4lem4  14347  cshweqdifid  14870  fsumsplit1  15795  fprodsplit1f  16040  catcone0  17747  efgred  19792  srgbinom  20260  c0mgm  20487  c0mhm  20488  lmodfopne  20922  ring2idlqus1  21354  m1detdiag  22626  1elcpmat  22744  phtpcer  25048  pntrlog2bndlem2  27642  wlkres  29708  clwwlkf  30081  hvpncan  31073  chsupsn  31447  ssjo  31481  elim2ifim  32570  rrhre  33969  pmeasadd  34292  bnj596  34724  bnj1209  34774  bnj996  34934  bnj1110  34960  bnj1189  34987  swrdrevpfx  35086  pfxwlk  35093  cusgr3cyclex  35106  satefvfmla0  35388  satefvfmla1  35395  arg-ax  36384  unirep  37676  idomnnzpownz  42091  ringexp0nn  42093  sn-sup2  42449  rp-isfinite6  43482  clsk1indlem2  44006  ntrclsss  44027  clsneiel1  44072  monoords  45214  fmul01  45503  fmuldfeqlem1  45505  fmuldfeq  45506  fmul01lt1lem1  45507  icccncfext  45810  iblspltprt  45896  stoweidlem3  45926  stoweidlem17  45940  stoweidlem19  45942  stoweidlem20  45943  stoweidlem23  45946  stirlinglem15  46011  fourierdlem16  46046  fourierdlem21  46051  fourierdlem72  46101  fourierdlem89  46118  fourierdlem90  46119  fourierdlem91  46120  hoidmvlelem4  46521  salpreimagelt  46630  salpreimalegt  46632  simpcntrab  46793  zeoALTV  47546  2zrngnmrid  47981  mndpsuppss  48098  linc0scn0  48154  eenglngeehlnm  48475  indthinc  48725  indthincALT  48726