Theorem ancli 552

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  barbariALT  2673  n0rex  4253  swopo  5463  xpdifid  6010  xpima  6024  elrnrexdm  6877  ixpsnf1o  8560  inf3lem6  9181  rankuni  9377  cardprclem  9493  nqpr  10526  letrp1  11574  p1le  11575  sup2  11686  peano2uz2  12163  uzind  12167  qreccl  12463  xrsupsslem  12795  supxrunb1  12807  faclbnd4lem4  13760  cshweqdifid  14283  fprodsplit1f  15448  catcone0  17073  efgred  19004  srgbinom  19426  lmodfopne  19803  m1detdiag  21360  1elcpmat  21478  phtpcer  23759  pntrlog2bndlem2  26326  wlkres  27624  clwwlkf  27996  hvpncan  28986  chsupsn  29360  ssjo  29394  elim2ifim  30474  rrhre  31553  pmeasadd  31874  bnj596  32308  bnj1209  32359  bnj996  32519  bnj1110  32545  bnj1189  32572  swrdrevpfx  32661  pfxwlk  32668  cusgr3cyclex  32681  satefvfmla0  32963  satefvfmla1  32970  arg-ax  34260  unirep  35526  sn-sup2  40056  rp-isfinite6  40719  clsk1indlem2  41238  ntrclsss  41259  clsneiel1  41304  monoords  42414  fsumsplit1  42695  fmul01  42703  fmuldfeqlem1  42705  fmuldfeq  42706  fmul01lt1lem1  42707  icccncfext  43010  iblspltprt  43096  stoweidlem3  43126  stoweidlem17  43140  stoweidlem19  43142  stoweidlem20  43143  stoweidlem23  43146  stirlinglem15  43211  fourierdlem16  43246  fourierdlem21  43251  fourierdlem72  43301  fourierdlem89  43318  fourierdlem90  43319  fourierdlem91  43320  hoidmvlelem4  43718  salpreimagelt  43824  salpreimalegt  43826  simpcntrab  43965  zeoALTV  44703  c0mgm  45048  c0mhm  45049  2zrngnmrid  45089  mndpsuppss  45288  linc0scn0  45345  eenglngeehlnm  45666  indthinc  45844  indthincALT  45845