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  2695  n0rex  4305  swopo  5570  xpdifid  6159  xpdifcnvepel  6160  xpima  6174  elrnrexdm  7089  mapex  7952  ixpsnf1o  8966  inf3lem6  9634  rankuni  9879  cardprclem  10060  nqpr  11099  letrp1  12161  p1le  12162  sup2  12273  peano2uz2  12787  uzind  12791  qreccl  13097  xrsupsslem  13437  supxrunb1  13449  faclbnd4lem4  14440  swrdrevpfx  14918  cshweqdifid  14971  fsumsplit1  15911  fprodsplit1f  16157  catcone0  17861  mndpsuppss  18959  efgred  19962  srgbinom  20457  c0mgm  20689  c0mhm  20690  lmodfopne  21175  ring2idlqus1  21615  m1detdiag  22912  1elcpmat  23033  phtpcer  25316  pntrlog2bndlem2  27905  wlkres  30249  pfxwlk  30266  clwwlkf  30638  hvpncan  31641  chsupsn  32015  ssjo  32049  elim2ifim  33141  rrhre  34653  pmeasadd  34957  bnj596  35377  bnj1209  35426  bnj996  35586  bnj1110  35612  bnj1189  35639  cusgr3cyclex  35911  satefvfmla0  36183  satefvfmla1  36190  arg-ax  37204  unirep  38648  idomnnzpownz  43182  ringexp0nn  43184  sn-sup2  43555  rp-isfinite6  44518  clsk1indlem2  45041  ntrclsss  45062  clsneiel1  45107  monoords  46312  fmul01  46591  fmuldfeqlem1  46593  fmuldfeq  46594  fmul01lt1lem1  46595  icccncfext  46896  iblspltprt  46982  stoweidlem3  47012  stoweidlem17  47026  stoweidlem19  47028  stoweidlem20  47029  stoweidlem23  47032  stirlinglem15  47097  fourierdlem16  47132  fourierdlem21  47137  fourierdlem72  47187  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  hoidmvlelem4  47607  salpreimagelt  47716  salpreimalegt  47718  simpcntrab  47879  zeoALTV  48767  2zrngnmrid  49352  linc0scn0  49534  eenglngeehlnm  49850  indthinc  50569  indthincALT  50570