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  2663  n0rex  4308  swopo  5538  xpdifid  6117  xpima  6131  elrnrexdm  7023  mapex  7874  ixpsnf1o  8865  inf3lem6  9529  rankuni  9759  cardprclem  9875  nqpr  10908  letrp1  11968  p1le  11969  sup2  12081  peano2uz2  12564  uzind  12568  qreccl  12870  xrsupsslem  13209  supxrunb1  13221  faclbnd4lem4  14203  cshweqdifid  14726  fsumsplit1  15652  fprodsplit1f  15897  catcone0  17593  mndpsuppss  18639  efgred  19627  srgbinom  20116  c0mgm  20344  c0mhm  20345  lmodfopne  20803  ring2idlqus1  21226  m1detdiag  22482  1elcpmat  22600  phtpcer  24892  pntrlog2bndlem2  27487  wlkres  29614  clwwlkf  29991  hvpncan  30983  chsupsn  31357  ssjo  31391  elim2ifim  32489  rrhre  33994  pmeasadd  34299  bnj596  34719  bnj1209  34769  bnj996  34929  bnj1110  34955  bnj1189  34982  swrdrevpfx  35100  pfxwlk  35107  cusgr3cyclex  35119  satefvfmla0  35401  satefvfmla1  35408  arg-ax  36400  unirep  37704  idomnnzpownz  42115  ringexp0nn  42117  sn-sup2  42474  rp-isfinite6  43501  clsk1indlem2  44025  ntrclsss  44046  clsneiel1  44091  monoords  45289  fmul01  45571  fmuldfeqlem1  45573  fmuldfeq  45574  fmul01lt1lem1  45575  icccncfext  45878  iblspltprt  45964  stoweidlem3  45994  stoweidlem17  46008  stoweidlem19  46010  stoweidlem20  46011  stoweidlem23  46014  stirlinglem15  46079  fourierdlem16  46114  fourierdlem21  46119  fourierdlem72  46169  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  hoidmvlelem4  46589  salpreimagelt  46698  salpreimalegt  46700  simpcntrab  46861  zeoALTV  47664  2zrngnmrid  48250  linc0scn0  48418  eenglngeehlnm  48734  indthinc  49457  indthincALT  49458