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  2668  n0rex  4307  swopo  5541  xpdifid  6124  xpima  6138  elrnrexdm  7032  mapex  7881  ixpsnf1o  8874  inf3lem6  9540  rankuni  9773  cardprclem  9889  nqpr  10923  letrp1  11983  p1le  11984  sup2  12096  peano2uz2  12578  uzind  12582  qreccl  12880  xrsupsslem  13220  supxrunb1  13232  faclbnd4lem4  14217  cshweqdifid  14741  fsumsplit1  15666  fprodsplit1f  15911  catcone0  17608  mndpsuppss  18688  efgred  19675  srgbinom  20164  c0mgm  20393  c0mhm  20394  lmodfopne  20849  ring2idlqus1  21272  m1detdiag  22539  1elcpmat  22657  phtpcer  24948  pntrlog2bndlem2  27543  wlkres  29691  clwwlkf  30071  hvpncan  31063  chsupsn  31437  ssjo  31471  elim2ifim  32569  rrhre  34127  pmeasadd  34431  bnj596  34851  bnj1209  34901  bnj996  35061  bnj1110  35087  bnj1189  35114  swrdrevpfx  35260  pfxwlk  35267  cusgr3cyclex  35279  satefvfmla0  35561  satefvfmla1  35568  arg-ax  36559  unirep  37854  idomnnzpownz  42325  ringexp0nn  42327  sn-sup2  42688  rp-isfinite6  43701  clsk1indlem2  44225  ntrclsss  44246  clsneiel1  44291  monoords  45487  fmul01  45768  fmuldfeqlem1  45770  fmuldfeq  45771  fmul01lt1lem1  45772  icccncfext  46073  iblspltprt  46159  stoweidlem3  46189  stoweidlem17  46203  stoweidlem19  46205  stoweidlem20  46206  stoweidlem23  46209  stirlinglem15  46274  fourierdlem16  46309  fourierdlem21  46314  fourierdlem72  46364  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  hoidmvlelem4  46784  salpreimagelt  46893  salpreimalegt  46895  simpcntrab  47056  zeoALTV  47858  2zrngnmrid  48444  linc0scn0  48611  eenglngeehlnm  48927  indthinc  49649  indthincALT  49650