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  2669  n0rex  4364  swopo  5609  xpdifid  6193  xpima  6207  elrnrexdm  7113  mapex  7968  ixpsnf1o  8983  inf3lem6  9677  rankuni  9907  cardprclem  10023  nqpr  11058  letrp1  12115  p1le  12116  sup2  12228  peano2uz2  12710  uzind  12714  qreccl  13015  xrsupsslem  13352  supxrunb1  13364  faclbnd4lem4  14338  cshweqdifid  14861  fsumsplit1  15784  fprodsplit1f  16029  catcone0  17738  mndpsuppss  18797  efgred  19787  srgbinom  20255  c0mgm  20482  c0mhm  20483  lmodfopne  20921  ring2idlqus1  21353  m1detdiag  22625  1elcpmat  22743  phtpcer  25049  pntrlog2bndlem2  27645  wlkres  29711  clwwlkf  30089  hvpncan  31081  chsupsn  31455  ssjo  31489  elim2ifim  32579  rrhre  33997  pmeasadd  34320  bnj596  34752  bnj1209  34802  bnj996  34962  bnj1110  34988  bnj1189  35015  swrdrevpfx  35114  pfxwlk  35121  cusgr3cyclex  35133  satefvfmla0  35415  satefvfmla1  35422  arg-ax  36411  unirep  37713  idomnnzpownz  42126  ringexp0nn  42128  sn-sup2  42492  rp-isfinite6  43522  clsk1indlem2  44046  ntrclsss  44067  clsneiel1  44112  monoords  45260  fmul01  45547  fmuldfeqlem1  45549  fmuldfeq  45550  fmul01lt1lem1  45551  icccncfext  45854  iblspltprt  45940  stoweidlem3  45970  stoweidlem17  45984  stoweidlem19  45986  stoweidlem20  45987  stoweidlem23  45990  stirlinglem15  46055  fourierdlem16  46090  fourierdlem21  46095  fourierdlem72  46145  fourierdlem89  46162  fourierdlem90  46163  fourierdlem91  46164  hoidmvlelem4  46565  salpreimagelt  46674  salpreimalegt  46676  simpcntrab  46837  zeoALTV  47606  2zrngnmrid  48121  linc0scn0  48290  eenglngeehlnm  48610  indthinc  48874  indthincALT  48875