Theorem ancli 572

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 553	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 196  df-an 385

This theorem is referenced by:  pm4.45im  583  barbari  2555  cesaro  2561  camestros  2562  calemos  2572  swopo  4969  xpdifid  5481  xpima  5495  elrnrexdm  6271  ixpsnf1o  7834  php4  8032  ssnnfi  8064  inf3lem6  8413  rankuni  8609  cardprclem  8688  nqpr  9715  letrp1  10744  p1le  10745  sup2  10858  peano2uz2  11341  uzind  11345  uzid  11578  qreccl  11684  xrsupsslem  12009  supxrunb1  12021  faclbnd4lem4  12945  cshweqdifid  13417  fprodsplit1f  14560  idghm  17498  efgred  17984  srgbinom  18368  subrgid  18605  lmodfopne  18724  m1detdiag  20222  1elcpmat  20339  phtpcer  22602  phtpcerOLD  22603  pntrlog2bndlem2  25067  wlkon  26061  trlon  26070  pthon  26105  spthon  26112  constr3lem6  26177  clwwlkf  26322  hvpncan  27280  chsupsn  27656  ssjo  27690  elim2ifim  28748  rrhre  29393  pmeasadd  29714  bnj596  30070  bnj1209  30121  bnj996  30279  bnj1110  30304  bnj1189  30331  arg-ax  31585  bj-mo3OLD  32022  unirep  32677  rp-isfinite6  36883  clsk1indlem2  37360  ntrclsss  37381  clsneiel1  37426  monoords  38452  fsumsplit1  38639  fmul01  38647  fmuldfeqlem1  38649  fmuldfeq  38650  fmul01lt1lem1  38651  icccncfext  38773  iblspltprt  38865  stoweidlem3  38896  stoweidlem17  38910  stoweidlem19  38912  stoweidlem20  38913  stoweidlem23  38916  stirlinglem15  38981  fourierdlem16  39016  fourierdlem21  39021  fourierdlem72  39071  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  hoidmvlelem4  39488  salpreimalegt  39597  zeoALTV  40119  n0rex  40310  1wlkres  40879  clwwlksf  41222  0pthon-av  41295  c0mgm  41699  c0mhm  41700  2zrngnmrid  41740  mndpsuppss  41946  linc0scn0  42006