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  2664  n0rex  4319  swopo  5561  xpdifid  6125  xpima  6139  elrnrexdm  7044  ixpsnf1o  8883  inf3lem6  9578  rankuni  9808  cardprclem  9924  nqpr  10959  letrp1  12008  p1le  12009  sup2  12120  peano2uz2  12600  uzind  12604  qreccl  12903  xrsupsslem  13236  supxrunb1  13248  faclbnd4lem4  14206  cshweqdifid  14720  fsumsplit1  15641  fprodsplit1f  15884  catcone0  17581  efgred  19544  srgbinom  19976  lmodfopne  20417  m1detdiag  21983  1elcpmat  22101  phtpcer  24395  pntrlog2bndlem2  26963  wlkres  28681  clwwlkf  29054  hvpncan  30044  chsupsn  30418  ssjo  30452  elim2ifim  31531  rrhre  32691  pmeasadd  33014  bnj596  33447  bnj1209  33497  bnj996  33657  bnj1110  33683  bnj1189  33710  swrdrevpfx  33797  pfxwlk  33804  cusgr3cyclex  33817  satefvfmla0  34099  satefvfmla1  34106  arg-ax  34964  unirep  36245  sn-sup2  40996  rp-isfinite6  41912  clsk1indlem2  42436  ntrclsss  42457  clsneiel1  42502  monoords  43652  fmul01  43941  fmuldfeqlem1  43943  fmuldfeq  43944  fmul01lt1lem1  43945  icccncfext  44248  iblspltprt  44334  stoweidlem3  44364  stoweidlem17  44378  stoweidlem19  44380  stoweidlem20  44381  stoweidlem23  44384  stirlinglem15  44449  fourierdlem16  44484  fourierdlem21  44489  fourierdlem72  44539  fourierdlem89  44556  fourierdlem90  44557  fourierdlem91  44558  hoidmvlelem4  44959  salpreimagelt  45068  salpreimalegt  45070  simpcntrab  45231  zeoALTV  45982  c0mgm  46327  c0mhm  46328  2zrngnmrid  46368  mndpsuppss  46567  linc0scn0  46624  eenglngeehlnm  46945  indthinc  47192  indthincALT  47193