Theorem ancli 550

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  barbariALT  2666  n0rex  4355  swopo  5600  xpdifid  6168  xpima  6182  elrnrexdm  7091  ixpsnf1o  8932  inf3lem6  9628  rankuni  9858  cardprclem  9974  nqpr  11009  letrp1  12058  p1le  12059  sup2  12170  peano2uz2  12650  uzind  12654  qreccl  12953  xrsupsslem  13286  supxrunb1  13298  faclbnd4lem4  14256  cshweqdifid  14770  fsumsplit1  15691  fprodsplit1f  15934  catcone0  17631  efgred  19616  srgbinom  20054  lmodfopne  20510  m1detdiag  22099  1elcpmat  22217  phtpcer  24511  pntrlog2bndlem2  27081  wlkres  28927  clwwlkf  29300  hvpncan  30292  chsupsn  30666  ssjo  30700  elim2ifim  31777  rrhre  33001  pmeasadd  33324  bnj596  33757  bnj1209  33807  bnj996  33967  bnj1110  33993  bnj1189  34020  swrdrevpfx  34107  pfxwlk  34114  cusgr3cyclex  34127  satefvfmla0  34409  satefvfmla1  34416  arg-ax  35301  unirep  36582  sn-sup2  41342  rp-isfinite6  42269  clsk1indlem2  42793  ntrclsss  42814  clsneiel1  42859  monoords  44007  fmul01  44296  fmuldfeqlem1  44298  fmuldfeq  44299  fmul01lt1lem1  44300  icccncfext  44603  iblspltprt  44689  stoweidlem3  44719  stoweidlem17  44733  stoweidlem19  44735  stoweidlem20  44736  stoweidlem23  44739  stirlinglem15  44804  fourierdlem16  44839  fourierdlem21  44844  fourierdlem72  44894  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  hoidmvlelem4  45314  salpreimagelt  45423  salpreimalegt  45425  simpcntrab  45586  zeoALTV  46338  c0mgm  46708  c0mhm  46709  ring2idlqus1  46804  2zrngnmrid  46848  mndpsuppss  47047  linc0scn0  47104  eenglngeehlnm  47425  indthinc  47672  indthincALT  47673