Theorem ancli 551

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  equsb1vOLDOLD  2513  barbariALT  2753  n0rex  4313  swopo  5483  xpdifid  6024  xpima  6038  elrnrexdm  6854  ixpsnf1o  8501  inf3lem6  9095  rankuni  9291  cardprclem  9407  nqpr  10435  letrp1  11483  p1le  11484  sup2  11596  peano2uz2  12069  uzind  12073  uzid  12257  qreccl  12367  xrsupsslem  12699  supxrunb1  12711  faclbnd4lem4  13655  cshweqdifid  14181  fprodsplit1f  15343  efgred  18873  srgbinom  19294  lmodfopne  19671  m1detdiag  21205  1elcpmat  21322  phtpcer  23598  pntrlog2bndlem2  26153  wlkres  27451  clwwlkf  27825  hvpncan  28815  chsupsn  29189  ssjo  29223  elim2ifim  30299  rrhre  31262  pmeasadd  31583  bnj596  32017  bnj1209  32068  bnj996  32228  bnj1110  32254  bnj1189  32281  swrdrevpfx  32363  pfxwlk  32370  cusgr3cyclex  32383  satefvfmla0  32665  satefvfmla1  32672  arg-ax  33764  unirep  34987  rp-isfinite6  39882  clsk1indlem2  40390  ntrclsss  40411  clsneiel1  40456  monoords  41562  fsumsplit1  41851  fmul01  41859  fmuldfeqlem1  41861  fmuldfeq  41862  fmul01lt1lem1  41863  icccncfext  42168  iblspltprt  42256  stoweidlem3  42287  stoweidlem17  42301  stoweidlem19  42303  stoweidlem20  42304  stoweidlem23  42307  stirlinglem15  42372  fourierdlem16  42407  fourierdlem21  42412  fourierdlem72  42462  fourierdlem89  42479  fourierdlem90  42480  fourierdlem91  42481  hoidmvlelem4  42879  salpreimagelt  42985  salpreimalegt  42987  simpcntrab  43126  zeoALTV  43834  c0mgm  44179  c0mhm  44180  2zrngnmrid  44220  mndpsuppss  44418  linc0scn0  44477  eenglngeehlnm  44725