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  2671  n0rex  4298  swopo  5544  xpdifid  6127  xpima  6141  elrnrexdm  7036  mapex  7886  ixpsnf1o  8880  inf3lem6  9548  rankuni  9781  cardprclem  9897  nqpr  10931  letrp1  11993  p1le  11994  sup2  12106  peano2uz2  12611  uzind  12615  qreccl  12913  xrsupsslem  13253  supxrunb1  13265  faclbnd4lem4  14252  cshweqdifid  14776  fsumsplit1  15701  fprodsplit1f  15949  catcone0  17647  mndpsuppss  18727  efgred  19717  srgbinom  20206  c0mgm  20433  c0mhm  20434  lmodfopne  20889  ring2idlqus1  21312  m1detdiag  22575  1elcpmat  22693  phtpcer  24975  pntrlog2bndlem2  27558  wlkres  29755  clwwlkf  30135  hvpncan  31128  chsupsn  31502  ssjo  31536  elim2ifim  32633  rrhre  34184  pmeasadd  34488  bnj596  34908  bnj1209  34957  bnj996  35117  bnj1110  35143  bnj1189  35170  swrdrevpfx  35318  pfxwlk  35325  cusgr3cyclex  35337  satefvfmla0  35619  satefvfmla1  35626  arg-ax  36617  unirep  38052  idomnnzpownz  42588  ringexp0nn  42590  sn-sup2  42953  rp-isfinite6  43966  clsk1indlem2  44490  ntrclsss  44511  clsneiel1  44556  monoords  45751  fmul01  46031  fmuldfeqlem1  46033  fmuldfeq  46034  fmul01lt1lem1  46035  icccncfext  46336  iblspltprt  46422  stoweidlem3  46452  stoweidlem17  46466  stoweidlem19  46468  stoweidlem20  46469  stoweidlem23  46472  stirlinglem15  46537  fourierdlem16  46572  fourierdlem21  46577  fourierdlem72  46627  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  hoidmvlelem4  47047  salpreimagelt  47156  salpreimalegt  47158  simpcntrab  47319  zeoALTV  48161  2zrngnmrid  48747  linc0scn0  48914  eenglngeehlnm  49230  indthinc  49952  indthincALT  49953