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  4311  swopo  5551  xpdifid  6134  xpima  6148  elrnrexdm  7043  mapex  7893  ixpsnf1o  8888  inf3lem6  9554  rankuni  9787  cardprclem  9903  nqpr  10937  letrp1  11997  p1le  11998  sup2  12110  peano2uz2  12592  uzind  12596  qreccl  12894  xrsupsslem  13234  supxrunb1  13246  faclbnd4lem4  14231  cshweqdifid  14755  fsumsplit1  15680  fprodsplit1f  15925  catcone0  17622  mndpsuppss  18702  efgred  19692  srgbinom  20181  c0mgm  20410  c0mhm  20411  lmodfopne  20866  ring2idlqus1  21289  m1detdiag  22556  1elcpmat  22674  phtpcer  24965  pntrlog2bndlem2  27560  wlkres  29758  clwwlkf  30138  hvpncan  31131  chsupsn  31505  ssjo  31539  elim2ifim  32636  rrhre  34203  pmeasadd  34507  bnj596  34927  bnj1209  34976  bnj996  35136  bnj1110  35162  bnj1189  35189  swrdrevpfx  35337  pfxwlk  35344  cusgr3cyclex  35356  satefvfmla0  35638  satefvfmla1  35645  arg-ax  36636  unirep  37969  idomnnzpownz  42506  ringexp0nn  42508  sn-sup2  42865  rp-isfinite6  43878  clsk1indlem2  44402  ntrclsss  44423  clsneiel1  44468  monoords  45663  fmul01  45944  fmuldfeqlem1  45946  fmuldfeq  45947  fmul01lt1lem1  45948  icccncfext  46249  iblspltprt  46335  stoweidlem3  46365  stoweidlem17  46379  stoweidlem19  46381  stoweidlem20  46382  stoweidlem23  46385  stirlinglem15  46450  fourierdlem16  46485  fourierdlem21  46490  fourierdlem72  46540  fourierdlem89  46557  fourierdlem90  46558  fourierdlem91  46559  hoidmvlelem4  46960  salpreimagelt  47069  salpreimalegt  47071  simpcntrab  47232  zeoALTV  48034  2zrngnmrid  48620  linc0scn0  48787  eenglngeehlnm  49103  indthinc  49825  indthincALT  49826