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 206  df-an 396

This theorem is referenced by:  barbariALT  2664  n0rex  4354  swopo  5599  xpdifid  6167  xpima  6181  elrnrexdm  7090  ixpsnf1o  8938  inf3lem6  9634  rankuni  9864  cardprclem  9980  nqpr  11015  letrp1  12065  p1le  12066  sup2  12177  peano2uz2  12657  uzind  12661  qreccl  12960  xrsupsslem  13293  supxrunb1  13305  faclbnd4lem4  14263  cshweqdifid  14777  fsumsplit1  15698  fprodsplit1f  15941  catcone0  17638  efgred  19664  srgbinom  20132  c0mgm  20357  c0mhm  20358  lmodfopne  20742  ring2idlqus1  21167  m1detdiag  22419  1elcpmat  22537  phtpcer  24841  pntrlog2bndlem2  27424  wlkres  29360  clwwlkf  29733  hvpncan  30725  chsupsn  31099  ssjo  31133  elim2ifim  32210  rrhre  33465  pmeasadd  33788  bnj596  34221  bnj1209  34271  bnj996  34431  bnj1110  34457  bnj1189  34484  swrdrevpfx  34571  pfxwlk  34578  cusgr3cyclex  34591  satefvfmla0  34873  satefvfmla1  34880  gg-cncrng  35647  gg-cnfld1  35648  arg-ax  35765  unirep  37046  sn-sup2  41805  rp-isfinite6  42732  clsk1indlem2  43256  ntrclsss  43277  clsneiel1  43322  monoords  44466  fmul01  44755  fmuldfeqlem1  44757  fmuldfeq  44758  fmul01lt1lem1  44759  icccncfext  45062  iblspltprt  45148  stoweidlem3  45178  stoweidlem17  45192  stoweidlem19  45194  stoweidlem20  45195  stoweidlem23  45198  stirlinglem15  45263  fourierdlem16  45298  fourierdlem21  45303  fourierdlem72  45353  fourierdlem89  45370  fourierdlem90  45371  fourierdlem91  45372  hoidmvlelem4  45773  salpreimagelt  45882  salpreimalegt  45884  simpcntrab  46045  zeoALTV  46797  2zrngnmrid  47093  mndpsuppss  47210  linc0scn0  47266  eenglngeehlnm  47587  indthinc  47834  indthincALT  47835