Theorem ancli 553

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  barbariALT  2673  n0rex  4286  swopo  5538  xpdifid  6120  xpima  6134  elrnrexdm  7031  mapex  7882  ixpsnf1o  8877  inf3lem6  9546  rankuni  9779  cardprclem  9895  nqpr  10929  letrp1  11991  p1le  11992  sup2  12104  peano2uz2  12609  uzind  12613  qreccl  12911  xrsupsslem  13251  supxrunb1  13263  faclbnd4lem4  14250  cshweqdifid  14774  fsumsplit1  15699  fprodsplit1f  15947  catcone0  17645  mndpsuppss  18725  efgred  19715  srgbinom  20204  c0mgm  20431  c0mhm  20432  lmodfopne  20891  ring2idlqus1  21313  m1detdiag  22581  1elcpmat  22699  phtpcer  24981  pntrlog2bndlem2  27560  wlkres  29756  clwwlkf  30136  hvpncan  31129  chsupsn  31503  ssjo  31537  elim2ifim  32634  rrhre  34214  pmeasadd  34518  bnj596  34938  bnj1209  34987  bnj996  35147  bnj1110  35173  bnj1189  35200  swrdrevpfx  35354  pfxwlk  35361  cusgr3cyclex  35373  satefvfmla0  35655  satefvfmla1  35662  arg-ax  36653  unirep  38090  idomnnzpownz  42626  ringexp0nn  42628  sn-sup2  42990  rp-isfinite6  43971  clsk1indlem2  44495  ntrclsss  44516  clsneiel1  44561  monoords  45753  fmul01  46033  fmuldfeqlem1  46035  fmuldfeq  46036  fmul01lt1lem1  46037  icccncfext  46338  iblspltprt  46424  stoweidlem3  46454  stoweidlem17  46468  stoweidlem19  46470  stoweidlem20  46471  stoweidlem23  46474  stirlinglem15  46539  fourierdlem16  46574  fourierdlem21  46579  fourierdlem72  46629  fourierdlem89  46646  fourierdlem90  46647  fourierdlem91  46648  hoidmvlelem4  47049  salpreimagelt  47158  salpreimalegt  47160  simpcntrab  47321  zeoALTV  48169  2zrngnmrid  48755  linc0scn0  48922  eenglngeehlnm  49238  indthinc  49960  indthincALT  49961