Theorem ancli 548

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  barbariALT  2664  n0rex  4322  swopo  5559  xpdifid  6143  xpima  6157  elrnrexdm  7063  mapex  7919  ixpsnf1o  8913  inf3lem6  9592  rankuni  9822  cardprclem  9938  nqpr  10973  letrp1  12032  p1le  12033  sup2  12145  peano2uz2  12628  uzind  12632  qreccl  12934  xrsupsslem  13273  supxrunb1  13285  faclbnd4lem4  14267  cshweqdifid  14791  fsumsplit1  15717  fprodsplit1f  15962  catcone0  17654  mndpsuppss  18698  efgred  19684  srgbinom  20146  c0mgm  20374  c0mhm  20375  lmodfopne  20812  ring2idlqus1  21235  m1detdiag  22490  1elcpmat  22608  phtpcer  24900  pntrlog2bndlem2  27495  wlkres  29604  clwwlkf  29982  hvpncan  30974  chsupsn  31348  ssjo  31382  elim2ifim  32480  rrhre  34017  pmeasadd  34322  bnj596  34742  bnj1209  34792  bnj996  34952  bnj1110  34978  bnj1189  35005  swrdrevpfx  35104  pfxwlk  35111  cusgr3cyclex  35123  satefvfmla0  35405  satefvfmla1  35412  arg-ax  36399  unirep  37703  idomnnzpownz  42115  ringexp0nn  42117  sn-sup2  42472  rp-isfinite6  43500  clsk1indlem2  44024  ntrclsss  44045  clsneiel1  44090  monoords  45288  fmul01  45571  fmuldfeqlem1  45573  fmuldfeq  45574  fmul01lt1lem1  45575  icccncfext  45878  iblspltprt  45964  stoweidlem3  45994  stoweidlem17  46008  stoweidlem19  46010  stoweidlem20  46011  stoweidlem23  46014  stirlinglem15  46079  fourierdlem16  46114  fourierdlem21  46119  fourierdlem72  46169  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  hoidmvlelem4  46589  salpreimagelt  46698  salpreimalegt  46700  simpcntrab  46861  zeoALTV  47661  2zrngnmrid  48234  linc0scn0  48402  eenglngeehlnm  48718  indthinc  49441  indthincALT  49442