Theorem ancli 555

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  barbariALT  2690  n0rex  4304  swopo  5559  xpdifid  6143  xpima  6157  elrnrexdm  7059  mapex  7910  ixpsnf1o  8909  inf3lem6  9578  rankuni  9811  cardprclem  9927  nqpr  10962  letrp1  12025  p1le  12026  sup2  12138  peano2uz2  12651  uzind  12655  qreccl  12960  xrsupsslem  13300  supxrunb1  13312  faclbnd4lem4  14299  cshweqdifid  14823  fsumsplit1  15748  fprodsplit1f  15996  catcone0  17695  mndpsuppss  18775  efgred  19764  srgbinom  20253  c0mgm  20480  c0mhm  20481  lmodfopne  20940  ring2idlqus1  21362  m1detdiag  22630  1elcpmat  22748  phtpcer  25030  pntrlog2bndlem2  27612  wlkres  29808  clwwlkf  30188  hvpncan  31181  chsupsn  31555  ssjo  31589  elim2ifim  32686  rrhre  34272  pmeasadd  34576  bnj596  34999  bnj1209  35048  bnj996  35208  bnj1110  35234  bnj1189  35261  swrdrevpfx  35415  pfxwlk  35422  cusgr3cyclex  35434  satefvfmla0  35716  satefvfmla1  35723  arg-ax  36724  unirep  38161  idomnnzpownz  42697  ringexp0nn  42699  sn-sup2  43061  rp-isfinite6  44042  clsk1indlem2  44566  ntrclsss  44587  clsneiel1  44632  monoords  45824  fmul01  46104  fmuldfeqlem1  46106  fmuldfeq  46107  fmul01lt1lem1  46108  icccncfext  46409  iblspltprt  46495  stoweidlem3  46525  stoweidlem17  46539  stoweidlem19  46541  stoweidlem20  46542  stoweidlem23  46545  stirlinglem15  46610  fourierdlem16  46645  fourierdlem21  46650  fourierdlem72  46700  fourierdlem89  46717  fourierdlem90  46718  fourierdlem91  46719  hoidmvlelem4  47120  salpreimagelt  47229  salpreimalegt  47231  simpcntrab  47392  zeoALTV  48240  2zrngnmrid  48826  linc0scn0  48993  eenglngeehlnm  49309  indthinc  50031  indthincALT  50032