Theorem ancli 558

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		ancli.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	jca 521	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  barbariALT  2694  n0rex  4305  swopo  5574  xpdifid  6160  xpdifcnvepel  6161  xpima  6175  elrnrexdm  7083  mapex  7938  ixpsnf1o  8948  inf3lem6  9615  rankuni  9848  cardprclem  9987  nqpr  11026  letrp1  12086  p1le  12087  sup2  12198  peano2uz2  12712  uzind  12716  qreccl  13022  xrsupsslem  13362  supxrunb1  13374  faclbnd4lem4  14363  swrdrevpfx  14841  cshweqdifid  14894  fsumsplit1  15834  fprodsplit1f  16080  catcone0  17778  mndpsuppss  18875  efgred  19878  srgbinom  20373  c0mgm  20603  c0mhm  20604  lmodfopne  21087  ring2idlqus1  21525  m1detdiag  22822  1elcpmat  22943  phtpcer  25226  pntrlog2bndlem2  27817  wlkres  30131  pfxwlk  30148  clwwlkf  30520  hvpncan  31523  chsupsn  31897  ssjo  31931  elim2ifim  33023  rrhre  34534  pmeasadd  34839  bnj596  35259  bnj1209  35308  bnj996  35468  bnj1110  35494  bnj1189  35521  cusgr3cyclex  35728  satefvfmla0  36000  satefvfmla1  36007  arg-ax  37038  unirep  38467  idomnnzpownz  43001  ringexp0nn  43003  sn-sup2  43382  rp-isfinite6  44361  clsk1indlem2  44885  ntrclsss  44906  clsneiel1  44951  monoords  46133  fmul01  46413  fmuldfeqlem1  46415  fmuldfeq  46416  fmul01lt1lem1  46417  icccncfext  46718  iblspltprt  46804  stoweidlem3  46834  stoweidlem17  46848  stoweidlem19  46850  stoweidlem20  46851  stoweidlem23  46854  stirlinglem15  46919  fourierdlem16  46954  fourierdlem21  46959  fourierdlem72  47009  fourierdlem89  47026  fourierdlem90  47027  fourierdlem91  47028  hoidmvlelem4  47429  salpreimagelt  47538  salpreimalegt  47540  simpcntrab  47701  zeoALTV  48589  2zrngnmrid  49174  linc0scn0  49356  eenglngeehlnm  49672  indthinc  50391  indthincALT  50392