Theorem ancli 549

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 512	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 206  df-an 397

This theorem is referenced by:  barbariALT  2672  n0rex  4289  swopo  5515  xpdifid  6076  xpima  6090  elrnrexdm  6974  ixpsnf1o  8735  inf3lem6  9400  rankuni  9630  cardprclem  9746  nqpr  10779  letrp1  11828  p1le  11829  sup2  11940  peano2uz2  12417  uzind  12421  qreccl  12718  xrsupsslem  13050  supxrunb1  13062  faclbnd4lem4  14019  cshweqdifid  14542  fsumsplit1  15466  fprodsplit1f  15709  catcone0  17405  efgred  19363  srgbinom  19790  lmodfopne  20170  m1detdiag  21755  1elcpmat  21873  phtpcer  24167  pntrlog2bndlem2  26735  wlkres  28047  clwwlkf  28420  hvpncan  29410  chsupsn  29784  ssjo  29818  elim2ifim  30897  rrhre  31980  pmeasadd  32301  bnj596  32735  bnj1209  32785  bnj996  32945  bnj1110  32971  bnj1189  32998  swrdrevpfx  33087  pfxwlk  33094  cusgr3cyclex  33107  satefvfmla0  33389  satefvfmla1  33396  arg-ax  34614  unirep  35880  sn-sup2  40446  rp-isfinite6  41132  clsk1indlem2  41659  ntrclsss  41680  clsneiel1  41725  monoords  42843  fmul01  43128  fmuldfeqlem1  43130  fmuldfeq  43131  fmul01lt1lem1  43132  icccncfext  43435  iblspltprt  43521  stoweidlem3  43551  stoweidlem17  43565  stoweidlem19  43567  stoweidlem20  43568  stoweidlem23  43571  stirlinglem15  43636  fourierdlem16  43671  fourierdlem21  43676  fourierdlem72  43726  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  hoidmvlelem4  44143  salpreimagelt  44252  salpreimalegt  44254  simpcntrab  44397  zeoALTV  45133  c0mgm  45478  c0mhm  45479  2zrngnmrid  45519  mndpsuppss  45718  linc0scn0  45775  eenglngeehlnm  46096  indthinc  46344  indthincALT  46345