Theorem ancli 547

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 510	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  barbariALT  2658  n0rex  4355  swopo  5600  xpdifid  6172  xpima  6186  elrnrexdm  7096  ixpsnf1o  8955  inf3lem6  9656  rankuni  9886  cardprclem  10002  nqpr  11037  letrp1  12088  p1le  12089  sup2  12200  peano2uz2  12680  uzind  12684  qreccl  12983  xrsupsslem  13318  supxrunb1  13330  faclbnd4lem4  14287  cshweqdifid  14802  fsumsplit1  15723  fprodsplit1f  15966  catcone0  17666  efgred  19707  srgbinom  20175  c0mgm  20402  c0mhm  20403  lmodfopne  20787  ring2idlqus1  21213  m1detdiag  22529  1elcpmat  22647  phtpcer  24951  pntrlog2bndlem2  27541  wlkres  29540  clwwlkf  29913  hvpncan  30905  chsupsn  31279  ssjo  31313  elim2ifim  32393  rrhre  33692  pmeasadd  34015  bnj596  34447  bnj1209  34497  bnj996  34657  bnj1110  34683  bnj1189  34710  swrdrevpfx  34796  pfxwlk  34803  cusgr3cyclex  34816  satefvfmla0  35098  satefvfmla1  35105  arg-ax  35970  unirep  37257  idomnnzpownz  41672  ringexp0nn  41674  sn-sup2  42089  rp-isfinite6  43013  clsk1indlem2  43537  ntrclsss  43558  clsneiel1  43603  monoords  44742  fmul01  45031  fmuldfeqlem1  45033  fmuldfeq  45034  fmul01lt1lem1  45035  icccncfext  45338  iblspltprt  45424  stoweidlem3  45454  stoweidlem17  45468  stoweidlem19  45470  stoweidlem20  45471  stoweidlem23  45474  stirlinglem15  45539  fourierdlem16  45574  fourierdlem21  45579  fourierdlem72  45629  fourierdlem89  45646  fourierdlem90  45647  fourierdlem91  45648  hoidmvlelem4  46049  salpreimagelt  46158  salpreimalegt  46160  simpcntrab  46321  zeoALTV  47073  2zrngnmrid  47430  mndpsuppss  47547  linc0scn0  47603  eenglngeehlnm  47924  indthinc  48170  indthincALT  48171