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  2697  n0rex  4308  swopo  5574  xpdifid  6165  xpdifcnvepel  6166  xpima  6180  elrnrexdm  7100  mapex  7962  ixpsnf1o  8980  inf3lem6  9647  rankuni  9892  cardprclem  10073  nqpr  11112  letrp1  12174  p1le  12175  sup2  12286  peano2uz2  12800  uzind  12804  qreccl  13110  xrsupsslem  13450  supxrunb1  13462  faclbnd4lem4  14453  swrdrevpfx  14932  cshweqdifid  14985  fsumsplit1  15926  fprodsplit1f  16172  catcone0  17876  mndpsuppss  18974  efgred  19977  srgbinom  20472  c0mgm  20704  c0mhm  20705  lmodfopne  21190  ring2idlqus1  21630  m1detdiag  22927  1elcpmat  23048  phtpcer  25331  pntrlog2bndlem2  27920  wlkres  30264  pfxwlk  30281  clwwlkf  30653  hvpncan  31656  chsupsn  32030  ssjo  32064  elim2ifim  33198  rrhre  34709  pmeasadd  35013  bnj596  35433  bnj1209  35482  bnj996  35642  bnj1110  35668  bnj1189  35695  scottidm  35823  cusgr3cyclex  36025  satefvfmla0  36307  satefvfmla1  36314  arg-ax  37334  unirep  38791  idomnnzpownz  43325  ringexp0nn  43327  sn-sup2  43698  rp-isfinite6  44662  clsk1indlem2  45185  ntrclsss  45206  clsneiel1  45251  monoords  46455  fmul01  46734  fmuldfeqlem1  46736  fmuldfeq  46737  fmul01lt1lem1  46738  icccncfext  47039  iblspltprt  47125  stoweidlem3  47155  stoweidlem17  47169  stoweidlem19  47171  stoweidlem20  47172  stoweidlem23  47175  stirlinglem15  47240  fourierdlem16  47275  fourierdlem21  47280  fourierdlem72  47330  fourierdlem89  47347  fourierdlem90  47348  fourierdlem91  47349  hoidmvlelem4  47750  salpreimagelt  47859  salpreimalegt  47861  simpcntrab  48022  zeoALTV  48910  2zrngnmrid  49495  linc0scn0  49677  indthinc  50739  indthincALT  50740