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  2664  n0rex  4328  swopo  5565  xpdifid  6149  xpima  6163  elrnrexdm  7068  mapex  7926  ixpsnf1o  8915  inf3lem6  9604  rankuni  9834  cardprclem  9950  nqpr  10985  letrp1  12042  p1le  12043  sup2  12155  peano2uz2  12638  uzind  12642  qreccl  12942  xrsupsslem  13280  supxrunb1  13292  faclbnd4lem4  14271  cshweqdifid  14795  fsumsplit1  15718  fprodsplit1f  15963  catcone0  17654  mndpsuppss  18698  efgred  19684  srgbinom  20146  c0mgm  20374  c0mhm  20375  lmodfopne  20812  ring2idlqus1  21235  m1detdiag  22490  1elcpmat  22608  phtpcer  24900  pntrlog2bndlem2  27496  wlkres  29605  clwwlkf  29983  hvpncan  30975  chsupsn  31349  ssjo  31383  elim2ifim  32481  rrhre  34019  pmeasadd  34324  bnj596  34744  bnj1209  34794  bnj996  34954  bnj1110  34980  bnj1189  35007  swrdrevpfx  35106  pfxwlk  35113  cusgr3cyclex  35125  satefvfmla0  35407  satefvfmla1  35414  arg-ax  36401  unirep  37705  idomnnzpownz  42112  ringexp0nn  42114  sn-sup2  42451  rp-isfinite6  43479  clsk1indlem2  44003  ntrclsss  44024  clsneiel1  44069  monoords  45268  fmul01  45551  fmuldfeqlem1  45553  fmuldfeq  45554  fmul01lt1lem1  45555  icccncfext  45858  iblspltprt  45944  stoweidlem3  45974  stoweidlem17  45988  stoweidlem19  45990  stoweidlem20  45991  stoweidlem23  45994  stirlinglem15  46059  fourierdlem16  46094  fourierdlem21  46099  fourierdlem72  46149  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  hoidmvlelem4  46569  salpreimagelt  46678  salpreimalegt  46680  simpcntrab  46841  zeoALTV  47626  2zrngnmrid  48173  linc0scn0  48341  eenglngeehlnm  48661  indthinc  49340  indthincALT  49341