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  4316  swopo  5550  xpdifid  6129  xpima  6143  elrnrexdm  7043  mapex  7897  ixpsnf1o  8888  inf3lem6  9562  rankuni  9792  cardprclem  9908  nqpr  10943  letrp1  12002  p1le  12003  sup2  12115  peano2uz2  12598  uzind  12602  qreccl  12904  xrsupsslem  13243  supxrunb1  13255  faclbnd4lem4  14237  cshweqdifid  14761  fsumsplit1  15687  fprodsplit1f  15932  catcone0  17628  mndpsuppss  18674  efgred  19662  srgbinom  20151  c0mgm  20379  c0mhm  20380  lmodfopne  20838  ring2idlqus1  21261  m1detdiag  22517  1elcpmat  22635  phtpcer  24927  pntrlog2bndlem2  27522  wlkres  29649  clwwlkf  30026  hvpncan  31018  chsupsn  31392  ssjo  31426  elim2ifim  32524  rrhre  34004  pmeasadd  34309  bnj596  34729  bnj1209  34779  bnj996  34939  bnj1110  34965  bnj1189  34992  swrdrevpfx  35097  pfxwlk  35104  cusgr3cyclex  35116  satefvfmla0  35398  satefvfmla1  35405  arg-ax  36397  unirep  37701  idomnnzpownz  42113  ringexp0nn  42115  sn-sup2  42472  rp-isfinite6  43500  clsk1indlem2  44024  ntrclsss  44045  clsneiel1  44090  monoords  45288  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  48237  linc0scn0  48405  eenglngeehlnm  48721  indthinc  49444  indthincALT  49445