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  2665  n0rex  4304  swopo  5533  xpdifid  6115  xpima  6129  elrnrexdm  7022  mapex  7871  ixpsnf1o  8862  inf3lem6  9523  rankuni  9756  cardprclem  9872  nqpr  10905  letrp1  11965  p1le  11966  sup2  12078  peano2uz2  12561  uzind  12565  qreccl  12867  xrsupsslem  13206  supxrunb1  13218  faclbnd4lem4  14203  cshweqdifid  14727  fsumsplit1  15652  fprodsplit1f  15897  catcone0  17593  mndpsuppss  18673  efgred  19660  srgbinom  20149  c0mgm  20377  c0mhm  20378  lmodfopne  20833  ring2idlqus1  21256  m1detdiag  22512  1elcpmat  22630  phtpcer  24921  pntrlog2bndlem2  27516  wlkres  29647  clwwlkf  30027  hvpncan  31019  chsupsn  31393  ssjo  31427  elim2ifim  32525  rrhre  34034  pmeasadd  34338  bnj596  34758  bnj1209  34808  bnj996  34968  bnj1110  34994  bnj1189  35021  swrdrevpfx  35161  pfxwlk  35168  cusgr3cyclex  35180  satefvfmla0  35462  satefvfmla1  35469  arg-ax  36460  unirep  37764  idomnnzpownz  42235  ringexp0nn  42237  sn-sup2  42594  rp-isfinite6  43621  clsk1indlem2  44145  ntrclsss  44166  clsneiel1  44211  monoords  45408  fmul01  45690  fmuldfeqlem1  45692  fmuldfeq  45693  fmul01lt1lem1  45694  icccncfext  45995  iblspltprt  46081  stoweidlem3  46111  stoweidlem17  46125  stoweidlem19  46127  stoweidlem20  46128  stoweidlem23  46131  stirlinglem15  46196  fourierdlem16  46231  fourierdlem21  46236  fourierdlem72  46286  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  hoidmvlelem4  46706  salpreimagelt  46815  salpreimalegt  46817  simpcntrab  46978  zeoALTV  47780  2zrngnmrid  48366  linc0scn0  48534  eenglngeehlnm  48850  indthinc  49573  indthincALT  49574