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  2670  n0rex  4309  swopo  5543  xpdifid  6126  xpima  6140  elrnrexdm  7034  mapex  7883  ixpsnf1o  8878  inf3lem6  9544  rankuni  9777  cardprclem  9893  nqpr  10927  letrp1  11987  p1le  11988  sup2  12100  peano2uz2  12582  uzind  12586  qreccl  12884  xrsupsslem  13224  supxrunb1  13236  faclbnd4lem4  14221  cshweqdifid  14745  fsumsplit1  15670  fprodsplit1f  15915  catcone0  17612  mndpsuppss  18692  efgred  19679  srgbinom  20168  c0mgm  20397  c0mhm  20398  lmodfopne  20853  ring2idlqus1  21276  m1detdiag  22543  1elcpmat  22661  phtpcer  24952  pntrlog2bndlem2  27547  wlkres  29744  clwwlkf  30124  hvpncan  31116  chsupsn  31490  ssjo  31524  elim2ifim  32622  rrhre  34180  pmeasadd  34484  bnj596  34904  bnj1209  34954  bnj996  35114  bnj1110  35140  bnj1189  35167  swrdrevpfx  35313  pfxwlk  35320  cusgr3cyclex  35332  satefvfmla0  35614  satefvfmla1  35621  arg-ax  36612  unirep  37917  idomnnzpownz  42408  ringexp0nn  42410  sn-sup2  42767  rp-isfinite6  43780  clsk1indlem2  44304  ntrclsss  44325  clsneiel1  44370  monoords  45566  fmul01  45847  fmuldfeqlem1  45849  fmuldfeq  45850  fmul01lt1lem1  45851  icccncfext  46152  iblspltprt  46238  stoweidlem3  46268  stoweidlem17  46282  stoweidlem19  46284  stoweidlem20  46285  stoweidlem23  46288  stirlinglem15  46353  fourierdlem16  46388  fourierdlem21  46393  fourierdlem72  46443  fourierdlem89  46460  fourierdlem90  46461  fourierdlem91  46462  hoidmvlelem4  46863  salpreimagelt  46972  salpreimalegt  46974  simpcntrab  47135  zeoALTV  47937  2zrngnmrid  48523  linc0scn0  48690  eenglngeehlnm  49006  indthinc  49728  indthincALT  49729