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

This theorem is referenced by:  barbariALT  2671  n0rex  4285  swopo  5505  xpdifid  6060  xpima  6074  elrnrexdm  6947  ixpsnf1o  8684  inf3lem6  9321  rankuni  9552  cardprclem  9668  nqpr  10701  letrp1  11749  p1le  11750  sup2  11861  peano2uz2  12338  uzind  12342  qreccl  12638  xrsupsslem  12970  supxrunb1  12982  faclbnd4lem4  13938  cshweqdifid  14461  fsumsplit1  15385  fprodsplit1f  15628  catcone0  17313  efgred  19269  srgbinom  19696  lmodfopne  20076  m1detdiag  21654  1elcpmat  21772  phtpcer  24064  pntrlog2bndlem2  26631  wlkres  27940  clwwlkf  28312  hvpncan  29302  chsupsn  29676  ssjo  29710  elim2ifim  30789  rrhre  31871  pmeasadd  32192  bnj596  32626  bnj1209  32676  bnj996  32836  bnj1110  32862  bnj1189  32889  swrdrevpfx  32978  pfxwlk  32985  cusgr3cyclex  32998  satefvfmla0  33280  satefvfmla1  33287  arg-ax  34532  unirep  35798  sn-sup2  40360  rp-isfinite6  41023  clsk1indlem2  41541  ntrclsss  41562  clsneiel1  41607  monoords  42726  fmul01  43011  fmuldfeqlem1  43013  fmuldfeq  43014  fmul01lt1lem1  43015  icccncfext  43318  iblspltprt  43404  stoweidlem3  43434  stoweidlem17  43448  stoweidlem19  43450  stoweidlem20  43451  stoweidlem23  43454  stirlinglem15  43519  fourierdlem16  43554  fourierdlem21  43559  fourierdlem72  43609  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  hoidmvlelem4  44026  salpreimagelt  44132  salpreimalegt  44134  simpcntrab  44273  zeoALTV  45010  c0mgm  45355  c0mhm  45356  2zrngnmrid  45396  mndpsuppss  45595  linc0scn0  45652  eenglngeehlnm  45973  indthinc  46221  indthincALT  46222