Theorem ancli 575

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 555	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  pm4.45im  586  barbari  2705  cesaro  2711  camestros  2712  calemos  2722  n0rex  4078  swopo  5197  xpdifid  5720  xpima  5734  elrnrexdm  6526  ixpsnf1o  8114  php4  8312  ssnnfi  8344  inf3lem6  8703  rankuni  8899  cardprclem  8995  nqpr  10028  letrp1  11057  p1le  11058  sup2  11171  peano2uz2  11657  uzind  11661  uzid  11894  qreccl  12001  xrsupsslem  12330  supxrunb1  12342  faclbnd4lem4  13277  cshweqdifid  13766  fprodsplit1f  14920  idghm  17876  efgred  18361  srgbinom  18745  subrgid  18984  lmodfopne  19103  m1detdiag  20605  1elcpmat  20722  phtpcer  22995  pntrlog2bndlem2  25466  wlkres  26777  clwwlkf  27176  hvpncan  28205  chsupsn  28581  ssjo  28615  elim2ifim  29671  rrhre  30374  pmeasadd  30696  bnj596  31123  bnj1209  31174  bnj996  31332  bnj1110  31357  bnj1189  31384  arg-ax  32721  bj-mo3OLD  33138  unirep  33820  rp-isfinite6  38366  clsk1indlem2  38842  ntrclsss  38863  clsneiel1  38908  monoords  40010  fsumsplit1  40307  fmul01  40315  fmuldfeqlem1  40317  fmuldfeq  40318  fmul01lt1lem1  40319  icccncfext  40603  iblspltprt  40692  stoweidlem3  40723  stoweidlem17  40737  stoweidlem19  40739  stoweidlem20  40740  stoweidlem23  40743  stirlinglem15  40808  fourierdlem16  40843  fourierdlem21  40848  fourierdlem72  40898  fourierdlem89  40915  fourierdlem90  40916  fourierdlem91  40917  hoidmvlelem4  41318  salpreimalegt  41426  zeoALTV  42091  c0mgm  42419  c0mhm  42420  2zrngnmrid  42460  mndpsuppss  42662  linc0scn0  42722